📐 Lean 4を用いた命題論理の証明：実践ガイド 🔗

この記事では、プログラミング言語であり定理証明支援系（Theorem Prover）でもある Lean 4 を用いて、命題論理の基本概念とその形式的な実装を技術的に解説していきます。

証明を形式化したい数学者であっても、型理論に飛び込もうとしているプログラマーであっても、本ガイドを通じて第一原理から論理を再構築することができます。基本的な論理定数から出発し、*「命題は型であり、証明はプログラムである」*という原則である**カリー＝ハワード同型対応（Curry-Howard Isomorphism）**を用いて、Lean 4がどのように論理構造をエレガントにモデル化するのかを探っていきましょう。

📑 目次 🔗

⚙️ プリアンブル：環境の準備 🔗

論理結合子を定義する前に、基盤となる環境をセットアップする必要があります。Lean 4では通常、スコープと計算時の振る舞いを制御する2つの特定のコマンドを使ってこれを行います。

namespace Basic

noncomputable section

• namespace Basic: このコマンドは定義をグループ化し、Leanの組み込みライブラリ（Prelude）との名前衝突を防ぎます。これにより、学習目的で True、False、And といった基本的な構造をゼロから再定義できるようになります。
• noncomputable section: Lean 4は定理証明支援系であると同時に、関数型プログラミング言語でもあります。そのためデフォルトでは、すべての定義に対して実行可能なバイトコードを生成しようとします。セクションを noncomputable（計算不能）としてマークすると、コンパイラにこのステップをスキップするよう指示します。これは実行時の動作よりも数学的性質に関心がある形式論理において一般的な手法です。

🧩 基本的な論理結合子 🔗

このセクションでは、標準的な数学の記法をLean 4のコードに対応させながら、論理の基礎要素を定義していきます。

✅ 1. 真：True (⊤) 🔗

最も単純な命題は、普遍的に論理的妥当性を持つ「真」です。プログラミングの用語で言えば、$\top$ は**ユニット型（Unit type）**のように振る舞います。つまり、状態をちょうど1つだけ持ち、追加のデータは何も保持しません。

定義：

inductive True : Prop where
  | intro : True

単一のコンストラクタ（intro）のみで定義されているため、True を「証明」する唯一の方法は、まさにこのコンストラクタを提供することです。

例：

-- Proving True unconditionally
example : True := True.intro

-- Any proposition 'a' trivially implies True
example {a : Prop} : a → True := fun _ => True.intro

❌ 2. 偽：False (⊥) 🔗

True が証明の自明な存在によって定義されるのに対し、False は証明が完全に存在しないことによって定義されます。これは空型（Empty type）（または Void型）にあたります。

定義：

inductive False : Prop

False にはコンストラクタが存在しないため、何もないところからインスタンス化することは絶対にできません。これは論理的な矛盾を表します。

爆発律（Ex Falso Quodlibet）： もし万が一 False の証明を手にすることができたなら、その時点で論理は崩壊し、どんな命題でも証明できるようになります。Leanでは再帰子（recursor）である False.elim を使ってこれを処理します。

-- From a falsehood, any proposition 'a' follows (⊥ → a)
def False.elim {a : Prop} (false_proof : False) : a := 
  false_proof.rec

🔄 3. 否定：Negation (¬) 🔗

Lean 4において、否定はプリミティブな組み込み概念ではありません。代わりに、含意（$\to$）と False を使って関数として定義されます。命題 $a$ が偽であること（$\neg a$ と表記）を証明するには、$a$ を仮定すると直接矛盾（$\bot$）が導かれるような関数を示す必要があります。

定義：

def Not (a : Prop) : Prop := a → False

主要な定理：

-- Proving Negation: If assuming 'a' proves False, then Not 'a' is true.
theorem Not.intro {a : Prop} (h : a → False) : Not a := 
  fun ha => h ha

-- Double Negation Introduction (a → ¬¬a)
theorem not_not_intro {a : Prop} (ha : a) : Not (Not a) := 
  fun na => na ha  -- 'na' has type (a → False), so passing 'ha' yields False.

-- Modus Tollens: If (a → b) and (¬b), then (¬a)
theorem Not.imp {a b : Prop} (nb : Not b) (ab : a → b) : Not a := 
  fun ha => 
    have hb : b := ab ha
    nb hb

➡️ 4. 含意：Implication (→) 🔗

Leanは型理論に基づいているため、論理的含意（$a \to b$）は文字通り関数として扱われます。$a$ ならば $b$ であることを証明するには、$a$ の任意の証明を受け取って $b$ の証明を返す関数を書けばよいのです。

連鎖的な含意の例： $c$ を $a$ に変換でき、さらに $b$ を $d$ に変換できるなら、$a \to b$ の関数を $c \to d$ の関数へと変換できます。

theorem imp_imp_imp {a b c d : Prop} 
  (ca : c → a) (bd : b → d) : (a → b) → (c → d) := 
  fun ab => fun hc => 
    have ha : a := ca hc
    have hb : b := ab ha
    bd hb

🔗 5. 連言（論理積）：Conjunction (∧) 🔗

$a$ と $b$ の両方が真であることを要求する連言（論理積）は、structure（構造体）としてモデル化されます。プログラミングの用語では、これは2つの別個の証拠を保持する直積型（Product type）（構造体やタプル）です。

定義：

structure And (a b : Prop) : Prop where
  intro ::
  left : a
  right : b

主要な証明パターン：

-- Introduction: Creating an And
example {a b : Prop} (ha : a) (hb : b) : And a b := 
  And.intro ha hb

-- Symmetry: a ∧ b → b ∧ a
theorem And.symm {a b : Prop} (h : And a b) : And b a := 
  And.intro h.right h.left

🔀 6. 選言（論理和）：Disjunction (∨) 🔗

選言（論理和）は、命題のうち少なくとも一方が真であることを要求します。And とは異なり、Or は帰納的な直和型（Sum type）（タグ付き共用体）です。なぜなら、証明を構築する方法として、明確に異なる2つの選択肢があるからです。

定義：

inductive Or (a b : Prop) : Prop where
  | inl (h : a) : Or a b
  | inr (h : b) : Or a b

$a \lor b$ を証明するには、$a$ の証明を inl（左注入：inject-left）コンストラクタで包むか、または $b$ の証明を inr（右注入：inject-right）コンストラクタで包みます。

例：

-- Symmetry: a ∨ b → b ∨ a
theorem Or.symm {a b : Prop} (h : Or a b) : Or b a :=
  match h with
  | Or.inl ha => Or.inr ha
  | Or.inr hb => Or.inl hb

↔️ 7. 論理的同値：Logical Equivalence (↔) 🔗

双条件（Bi-implication）、すなわち「必要十分条件（if and only if / Iff）」は、2つの命題が論理的に同値であることを表します。これは双方向の含意を保持する構造体として定義されます。

定義：

structure Iff (a b : Prop) : Prop where
  intro ::
  mp : a → b
  mpr : b → a

反射律の例：

-- Every proposition is equivalent to itself (a ↔ a)
theorem Iff.refl {a : Prop} : Iff a a :=
  Iff.intro (fun ha => ha) (fun ha => ha)

🎯 まとめと重要なポイント 🔗

Lean 4で命題論理をゼロから再構築することで、形式体系が持つ機械的な美しさが浮かび上がってきます。

1. デフォルトで конструкティブ（構成的）： 何かが真であると単に宣言するのではなく、真であることの*証拠（エビデンス）*を保持するとはどういうことかを定義します。
2. 型としての命題： カリー＝ハワード同型対応を通じて、論理結合子は標準的なプログラミングの構造に直接対応します。含意は関数、And は構造体、Or は列挙型（enum）、True はユニット型、そして False は空型（void）です。
3. プログラムとしての証明： Leanで数学の証明を書くことは、特定のシグネチャを満たす型安全な関数を書くことと完全に同一です。

これらの基礎的なビルディングブロックを習得することは、より複雑な数学の定理や述語論理、さらには複雑なソフトウェアシステムの形式検証に取り組むための極めて重要な足がかりとなります。