Lean 4 で学ぶ古典論理 ― 排中律・背理法と公理系

今回は Lean 4 の論理的な土台に目を向けてみます。Lean は基本的に直観主義論理を採用していますが、古典論理で使える「排中律」も標準ライブラリに用意されています。排中律の意味、背理法との関係、そして Lean が裏側で依存している公理系について、学習します。教材には引き続き「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」です。

直観主義論理と古典論理の違い

直観主義論理（Intuitionistic Logic）とは、命題の真偽を「実際に証拠（証人）を構成することで示す」という考え方に基づいた論理体系です。「ある値が存在する」と言いたければ、その値を具体的に取り出してみせなければなりません。

一方、古典論理（Classical Logic）では、「存在しないと仮定すると矛盾が生じる」という間接的な論法も許されています。この違いを生み出すのが、古典論理のみが無条件に認める排中律です。

排中律とは

排中律（Law of Excluded Middle）は、任意の命題 P に対して次が成り立つという主張です。

P ∨ ¬P

「どんな命題も、真か偽かのどちらかである」――一見当然のように思えますが、直観主義論理の観点では、この「どちらか」を証拠として示すことなく宣言しています。直観主義論理では、排中律は自明の公理ではなく、証明が必要な命題として扱われます。

背理法の仕組み

排中律があることで、背理法（Proof by Contradiction）という証明テクニックが使えるようになります。その仕組みは次のとおりです。

• 「A である」ことを証明したいとき、あえて「¬A（A ではない）」と仮定する。
• その仮定から矛盾が導かれるなら、「¬A」という可能性が崩れる。
• 排中律によって「A か ¬A かのどちらか」が保証されているので、¬A が否定された以上、「A である」が確定する。

Lean における排中律：Classical.em

Lean では、排中律は Classical.em という名前で定義されています。

theorem Classical.em (p : Prop) : p ∨ ¬p

これは Lean の標準ライブラリに含まれており、必要に応じて利用できます。ただし、このように古典論理の道具を使うと、証明が依存する公理が増えます。それを確認するのが次のコマンドです。

#print axioms で公理を確認する

#print axioms コマンドを使うと、指定した定理や定義がどの公理に依存しているかを一覧で確認できます。

#print axioms Classical.em
-- 'Classical.em' depends on axioms: [propext, Classical.choice, Quot.sound]

Classical.em は三つの公理に依存していることがわかります。それぞれの意味を順番に見ていきましょう。

三つの公理を読み解く

propext — 外延性公理

propext {a b : Prop} : (a ↔ b) → a = b

「同値な命題は等しい」という公理です。a ↔ b（a と b が同値）であれば a = b（a と b は等しい）と見なせる、という主張です。Lean では命題を型として扱うため、「型として等しい」ことは「完全に同じものである」ことを意味します。

Classical.choice — 選択原理

Classical.choice.{u} {α : Sort u} : Nonempty α → α

「空でない型 α に対して、その要素を一つ取り出せる」という公理です。有限の型だけでなく、無限の型に対しても認めます。ここが大きなポイントです。

無限の型から要素を「具体的に取り出す」手続きは実装できないため、Classical.choice を使った定義はプログラムとして実行不可能です。このような定義には noncomputable 修飾子が必要になります（後述）。

Quot.sound — 商の公理

Quot.sound.{u} {α : Sort u} {r : α → α → Prop} {a b : α} : r a b → Quot.mk r a = Quot.mk r b

「同値関係 r によって関連する要素 a と b は、商型（Quotient）の上で等しい」という公理です。数学における商集合の概念を Lean に取り込むために必要な公理で、Lean の商型（Quot）の構成を支えています。

noncomputable 修飾子

Classical.choice のように選択原理を使った定義は、「実際に計算できる」保証がありません。そのため、もし Classical.choice を利用して関数などを定義しようとすると、Lean は noncomputable 修飾子を要求します。

noncomputable def myFunc : ... := ...

これは「この定義は計算不可能であることを理解したうえで書いています」という明示的な宣言です。証明の世界では問題なく使えますが、実行可能なプログラムとして利用することはできません。通常のプログラミング言語では計算不可能を示す修飾子はないので、面白いところです。