命題論理¶
命題論理では，個々の命題 P Q R : Prop を対象にして，論理結合子
∧，∨，→，¬，↔，True，False を扱います．
Lean では，これらの論理記号も型として実装されています．
たとえば P → Q は「P の証明を受け取って Q の証明を返す関数型」です．
P ∧ Q は And P Q，P ∨ Q は Or P Q，P ↔ Q は Iff P Q の記法です．
また，¬ P は定義上 P → False の略記です．
したがって，論理結合子の導入規則は「その型の項を作る方法」，除去規則は「その型の項から情報を取り出して使う方法」と読めます．
この視点を持つと，constructor が導入規則，cases や .left，.right が除去規則に対応する理由が見えやすくなります．
仮定規則¶
すでに仮定 hP : P があるなら，結論 P はその仮定そのもので証明できます．
Lean では，仮定名を exact で渡します．
この規則は自然演繹では仮定規則，仮説規則，あるいは単に assumption rule と呼ばれます． 証明論の本では，前提をもたない初期規則という意味で axiom と表示されることもあります． 特にシーケント計算では，対応する規則を identity axiom や initial sequent と呼び，たとえば \(\Gamma, P \vdash P\) の形で書きます． したがって，紙の上の証明体系で「仮定規則を axiom と書く」こと自体はあります．
ただし，ここでの axiom は，Lean の axiom コマンドとは意味が違います．
hP : P は現在の証明の中で使ってよいローカルな仮定であり，exact hP はその仮定として与えられた証明項をそのまま使っています．
一方，Lean で axiom と宣言すると，証明を構成せずに大域的な定数を環境へ追加することになります．
これはローカルな仮定を使うことより強い操作なので，通常の証明中の hP : P とは区別します．
証明図:
具体例: 「\(n\) は偶数である」と仮定しているなら，証明の途中でそのまま「\(n\) は偶数である」と言ってよい，という規則です．
含意導入 → introduction¶
P → Q を証明するには，いったん P を仮定して，そのもとで Q を証明します．
Lean では intro hP により，ゴール P → Q を「仮定 hP : P のもとで Q を示す」というゴールに変えます．
証明図:
具体例: 「\(n\) が偶数なら \(n^2\) も偶数である」を示すとき，まず「\(n\) は偶数である」と仮定し，その仮定のもとで「\(n^2\) は偶数である」を示します．
含意除去 → elimination¶
含意除去は modus ponens です．
hPQ : P → Q と hP : P があれば，hPQ hP : Q が得られます．
証明図:
具体例: 「収束する数列は有界である」と「数列 \((a_n)\) は収束する」が分かっていれば，「\((a_n)\) は有界である」と結論できます．
連言導入 ∧ introduction¶
P ∧ Q を証明するには，P の証明と Q の証明を両方与えます．
Lean では constructor がゴールを P と Q の 2 つに分解します．
証明図:
具体例: 「\(x > 0\)」と「\(y > 0\)」をそれぞれ証明できれば，「\(x > 0\) かつ \(y > 0\)」を証明できます．
連言除去 ∧ elimination¶
h : P ∧ Q があるなら，左成分 h.left : P と右成分 h.right : Q を取り出せます．
証明図:
具体例: 「\(x > 0\) かつ \(y > 0\)」が分かっていれば，左成分として「\(x > 0\)」を取り出せますし，右成分として「\(y > 0\)」も取り出せます．
example (P Q : Prop) (h : P ∧ Q) : P := by
exact h.left
example (P Q : Prop) (h : P ∧ Q) : Q := by
exact h.right
選言導入 ∨ introduction¶
P ∨ Q を証明するには，左側の P を証明するか，右側の Q を証明すれば十分です．
Lean では左を選ぶとき Or.inl，右を選ぶとき Or.inr を使います．
証明図:
具体例: 「\(n = 0\)」が分かっていれば，「\(n = 0\) または \(n > 0\)」を結論できます． 同様に，「\(n > 0\)」が分かっている場合も「\(n = 0\) または \(n > 0\)」を結論できます．
example (P Q : Prop) (hP : P) : P ∨ Q := by
exact Or.inl hP
example (P Q : Prop) (hQ : Q) : P ∨ Q := by
exact Or.inr hQ
選言除去 ∨ elimination¶
h : P ∨ Q から R を示すには，P の場合に R が出ることと，Q の場合に R が出ることを両方示します．
Lean では cases h with により，左の場合と右の場合に場合分けします．
証明図:
具体例: 自然数 \(n\) について「\(n = 0\) または \(n > 0\)」が分かっていて，どちらの場合にも「\(n \ge 0\)」が言えるなら，結論として「\(n \ge 0\)」が言えます．
example (P Q R : Prop) (h : P ∨ Q) (hPR : P → R) (hQR : Q → R) : R := by
cases h with
| inl hP =>
exact hPR hP
| inr hQ =>
exact hQR hQ
真の導入 True introduction¶
True は常に証明できます．
Lean では True.intro が True の標準的な証明です．
証明図:
具体例:
どのような仮定のもとでも，論理的に常に正しい命題 True は証明できます．
数学の議論では，情報を持たない自明な結論を置く場合に対応します．
偽の除去 False elimination¶
False の証明があるなら，任意の命題 P を証明できます．
これは爆発律（ex falso quodlibet）と呼ばれます．
Lean では False.elim hFalse を使います．
証明図:
具体例: もし仮定から「\(0 = 1\)」のような矛盾が導けてしまったなら，その矛盾から任意の命題を導けます． もちろん，通常の一貫した数学では矛盾そのものを導けないように注意します．
否定導入 ¬ introduction¶
Lean では ¬ P は P → False の略記です．
したがって ¬ P を証明するには，P を仮定して矛盾 False を導きます．
証明図:
具体例: 「\(\sqrt{2}\) は有理数である」と仮定すると矛盾が出ることを示せば，「\(\sqrt{2}\) は有理数ではない」と結論できます．
否定除去 ¬ elimination¶
hP : P と hNotP : ¬ P が同時にあると，False が得られます．
さらに False.elim を使えば任意の結論を導けます．
証明図:
具体例:
同じ文脈で「\(x > 0\)」と「\(x > 0\) ではない」が同時に得られたら，矛盾 False が得られます．
example (P : Prop) (hP : P) (hNotP : ¬ P) : False := by
exact hNotP hP
example (P Q : Prop) (hP : P) (hNotP : ¬ P) : Q := by
exact False.elim (hNotP hP)
同値導入 ↔ introduction¶
P ↔ Q を証明するには，P → Q と Q → P の両方向を証明します．
Lean では constructor が 2 つの方向にゴールを分解します．
証明図:
具体例: 「\(P \land Q\) と \(Q \land P\) は同値である」を示すには，\(P \land Q\) から \(Q \land P\) を示す方向と，\(Q \land P\) から \(P \land Q\) を示す方向の両方を証明します．
example (P Q : Prop) (hPQ : P → Q) (hQP : Q → P) : P ↔ Q := by
constructor
· intro hP
exact hPQ hP
· intro hQ
exact hQP hQ
同値除去 ↔ elimination¶
h : P ↔ Q があるなら，h.mp : P → Q と h.mpr : Q → P を取り出せます．
名前の mp は modus ponens，mpr はその逆向きを表します．
証明図:
具体例: 「\(x = 0\) と \(x^2 = 0\) は同値である」が分かっているなら，\(x = 0\) から \(x^2 = 0\) を得られます． 逆向きに，\(x^2 = 0\) から \(x = 0\) を得ることもできます．
example (P Q : Prop) (h : P ↔ Q) (hP : P) : Q := by
exact h.mp hP
example (P Q : Prop) (h : P ↔ Q) (hQ : Q) : P := by
exact h.mpr hQ
古典論理: 排中律¶
Lean の基本的な推論規則は構成的に読めます．
構成的論理では，一般の命題 P について P ∨ ¬ P を無条件に証明することはできません．
そのため，排中律 P ∨ ¬ P や背理法を使うときは，古典論理を使っていることを意識します．
命題ごとの排中律は Classical.em P で得られます．
Mathlib では古典論理を使う定理や tactic がよく使われますが，ここでは構成的に証明できる規則と古典論理に依存する規則を分けて見ることが重要です．
証明図:
ここで LEM とは排中律（Law of Excluded Middle）のことです．
具体例: 古典論理では，任意の命題 \(P\) について「\(P\) が成り立つ，または \(P\) は成り立たない」と言えます． たとえば「ある方程式に解が存在する，または存在しない」という形の主張です．
古典論理: 背理法¶
古典論理では，¬ P を仮定すると矛盾が出ることから P を結論できます．
Core Lean では，この原理は Classical.byContradiction として使えます．
Classical.byContradiction は，¬ P → False から P を返します．
これは二重否定除去 ¬¬ P → P と同じ強さをもつため，一般には古典論理の原理です．
Mathlib を import している環境では，背理法用の便利な tactic として by_contra もよく使われますが，ここでは Core Lean の定理を直接使います．
証明図:
ここで RAA とは背理法（Reductio Ad Absurdum）のことです．
具体例: 「素数は無限に存在する」を背理法で示すとき，「素数は有限個しか存在しない」と仮定し，その仮定から矛盾を導いて，もとの命題を結論します．