Lean における論理１

Lean での証明に必要な論理やタクティクの基本を学習していきます。教材には引き続き「ゼロから始めるLean言語入門 手を動かして学ぶ形式数学ライブラリ開発」です。今回、命題、含意、否定といった基本的な論理概念と、その証明方法を学習します。

---

1. 命題（Proposition）

1.1 Prop型とは

Lean における命題は Prop型 です。命題というのは、真偽が定まる主張のことですね。以下のコードで確認してみましょう。

#check Prop
#check (1 + 1 = 3)

1.2 述語（Predicate）

述語というのは、変数に依存した命題です。以下の例を見てください。これは n によって「n+3が39と等しいか」が変わってくるので、述語というわけです。

#check (fun n => n + 3 = 39)

1.3 真偽値とProp

#check True
#check False

True と False はブール値ではなく 命題 です。小文字の true/false は真偽値（Bool型）で、大文字の True/False は命題（Prop型）という違いがあるので気をつけてください。

---

2. 簡単な証明

2.1 自明な命題：trivial タクティク

自明な命題を証明する時は trivial タクティクを使います。このタクティクは、事前に登録されている複数のタクティクを順に試してくれます。文字通り自明な時に使います。

example : True := by trivial

2.2 仮定から結論を引き出す：exact と assumption

命題 P の証明 h : P があるとき、当然ながら P を示すことができます。試しに証明してみましょう：

example (P : Prop) (h : P) : P := by
  exact h

exact タクティクは、手元にある前提や関数を組み合わせてゴールと全く同じ型のオブジェクトを作り、「これがその証明です！」と差し出すものです。ここでは h がまさに P の証明なので、これで証明完了ですね。

同じ処理は assumption タクティクでも可能です：

example (P : Prop) (h : P) : P := by
  assumption

---

3. 含意（Implication）

3.1 含意とは

含意は「P ならば Q」を表し、P → Q と書きます。感覚的には、P が成り立つならば Q も成り立つという意味ですね。

論理的な意味はこうです：

• P が成り立ち、かつ Q も成り立つ → P → Q は真
• P が成り立つが、Q は成り立たない → P → Q は偽
• P が成り立たない → P → Q は問答無用で真（仮定が偽なら含意も真）

実際に確認してみましょう：

#eval True → True    -- true
#eval True → False   -- false
#eval False → True   -- true
#eval False → False  -- true

3.2 含意を使う：apply タクティク

証明で含意を使うには apply タクティクを使用します。仮定 h : P → Q があり、ゴールが Q である時、apply h を実行するとゴールが P に変わります。試してみましょう：

example (P Q : Prop) (h : P → Q) (hp : P) : Q := by
  apply h
  apply hp

上記の例は、より簡潔に以下のように書くこともできます：

example (P Q : Prop) (h : P → Q) (hp : P) : Q := by
  exact h hp

3.3 含意の右結合性

Lean では含意は右結合的に振る舞います。つまり、複数の含意が続く場合は右から括られるということですね：

example (P Q R : Prop) : (P → Q → R) = (P → (Q → R)) := by
  rfl

つまり、P → Q → R は P → (Q → R) と同じ意味です。

3.4 含意を証明する：intro タクティク

含意を証明する際のタクティクで重要なものに intro があります。intro を使うことで含意 P ならば Q の P を仮定に加えることができて、後は Q を示せば良い状態になります。引数は仮定に名前をつけるためのもので、以下の例では h : P になりますね：

example (P Q : Prop) (hq : Q) : P → Q := by
  intro h
  exact hq

---

4. 否定（Negation）

4.1 否定の定義

最後に、否定についてです。否定は ¬ で表現します。以下のように評価してみると、直感通りですね：

#eval ¬ True   -- false
#eval ¬ False  -- true

4.2 否定と含意の関係

数学の典型的な推論「P を仮定すると矛盾するから P は偽である」を考えてみてください。これは Lean では以下のように表現されます：

example (P : Prop) : (¬ P) = (P → False) := by
  rfl

つまり、否定 ¬ P は実質的には P → False と同じということです。P が成り立つなら矛盾（False）が導かれるという意味ですね。

4.3 矛盾から何でも言える：contradiction タクティク

ここで大事な原理が出てきます。仮定に P と ¬ P の両方がある場合、明らかに矛盾します。そして矛盾があれば、どんな命題でも示すことができるんです。そのために contradiction というタクティクが用意されています：

example (P : Prop) (hnp : ¬ P) (hp : P) : False := by
  contradiction

このタクティクの動作は以下と同等です：

example (P : Prop) (hnp : ¬ P) (hp : P) : False := by
  apply hnp  -- ¬ P は P → False なので、P を示せば False が得られる
  exact hp   -- P は hp で示せる

4.4 ゴールを矛盾の証明に変更する：exfalso タクティク

どんな命題であっても、exfalso タクティクを使うと証明のゴールを「矛盾（False）を示すこと」に変更できます：

example (P Q : Prop) (hnp : ¬ P) (hp : P) : Q := by
  exfalso -- ⊢ False
  contradiction

これで、命題を直接証明する代わりに、その否定を仮定すると矛盾することを示すという背理法的なアプローチができるようになります。

---

まとめ

Lean における論理の基礎として、以下のポイントを学びました：

概念	記号	説明	主なタクティク
命題	Prop	真偽が定まる主張	trivial, exact, assumption
含意	P → Q	P ならば Q	apply, intro
否定	¬ P	NOT P（= P → False）	contradiction, exfalso

---

コード公開

本記事で扱ったコードは、以下のリポジトリで公開しています：

• https://github.com/ringring-creator/LearnLean

学習過程を示すものなので、ぜひ参考にしてみてください。