（再掲）La Mort de Socrate
- ソクラテスは人間である
- 人間はすべからく死ぬ
- ソクラテスは死ぬ
証明を言葉にして説明するのは簡単です。
死ぬ存在を示すには、 “Human_is_Mortal” により人間の存在を示せば十分です。一方で、人間の存在は “Socrates_is_Human” とソクラテスの存在から得ることが出来ます。従って死ぬ存在が示され、命題の証明が完了します。
また、演繹的な説明ももちろん可能です。ただし、この場合の証明は少し複雑なtacticsを用いることになるので今回は上の流れで記述を行います。
ソクラテスの存在が仮定されているので、 “Socrates_is_Human” により人間が結論付けられます。次に、 “Human_is_Mortal” により、人間から死ぬ存在であることを結論づけることが出来ます。
前者の論理説明をGlaceonを使って証明してみましょう。
Glaceonではルールとして “begin” ～ “end” の間の範囲のみ記述が許されていました。
“PならばQ” の形の主張ではまず P を仮定に持ち上げます。
主張の前条件を仮定に持ち上げるためのコマンドは “assume” です。下の証明エリアでは先にコマンドを配置してあります。
“assume Socrates,” の前後の行にカーソルを合わせて、証明の右エリアで途中の証明状況を確認してみてください。
“assume Socrates,” の次の行にカーソルをあわせると、証明途中は以下のような表示になっていると思います：
ゴールとなる目標は “is_mortal” を証明することです。
Socrates human is_mortal : Type,
Socrates_is_Human : Socrates → human,
Human_is_Mortal : human → is_mortal,
Socrates : Socrates
⊢ is_mortal上の状況を言葉で書き直すと以下のようになります：
[仮定]
（Socrates, human, is_mortal：型として宣言）
Socrates_is_Human : ソクラテスならば人間である
Human_is_Mortal : 人間ならば死ぬ存在である
Socrates : ソクラテスの存在は仮定されている
[ゴール]
is_mortal：死ぬ存在であることを証明せよこの状況から証明の続きを書いていきましょう。
“Human_is_Mortal” により人間の存在を示せば十分
これはtactic “apply” を用いて、”apply Human_is_Mortal” を使います。
人間の存在は “Socrates_is_Human” とソクラテスの存在から得られる
この場合もtactic “apply” を用いますが、 “PならばQ” 型の命題は関数的に使うことができます。この場合、”apply Socrates_is_Human Socrates” と記述することが可能です。
是非、自分で上の証明エリアを使って試してみてください。
証明が完全に完了すると、証明エリアの右下に “Solved!” と表示されるはずです。
完全な証明例は下記に記しておきます。
解答例
証明エリアの右下が “Solved!” と表示されていて、証明がプログラムによって確かめられたことが確認出来ます！
今回新しく学んだtacticsは以下の2つです：
- assume
- apply
(No liked Yet)