⇒と証明と定理
追加したい：証明図
○健全な研究室
さトぅー
「次はG0で必ず使える、論理式と推論規則よ」
エーリル
「必ず使えるってどういうこと？ 公理と違うの？」
さトぅー
「公理は自分で勝手に決めていいルール。
でも今からいうルールは絶対に変えたらダメ。
論理的公理っていうんだけど、これが変わると言語も変わる」
エーリル
「言語設定なら仕方ない」
さトぅー
「長くなるから論理式にAx1,Ax2,Ax3って名前をつける」
■G0で必ず使える論理式(論理的公理)
Ax1 (φ⇒(ψ⇒φ))
Ax2 ((φ⇒(ψ⇒ρ))⇒((φ⇒ψ)⇒(φ⇒ρ)))
Ax3 (((￢ψ)⇒(￢φ))⇒(φ⇒ψ))
さトぅー
「しつこく言うけど、Ax1,Ax2,Ax3は固定。普通の公理は論理的公理と別に設定する。
それと文の変形ができるような推論規則も必要ね」
■推論規則:⇒el
φ (φ⇒ψ)
--------[⇒el]
ψ
天々城
「elは除去の略だナ」
エーリル
「φと(φ⇒ψ)からψって文に変形できるっていうのが⇒elの定義？」
天々城
「大体そういうことだナ。
あとは仮定や結論を定義してないといけない」
■仮定と結論の定義
φ_1,...,φ_n,ψを論理式とする。
φ_1 .... φ_n
--------------[R]
ψ
となる推論規則Rがあるとき、ψはφ_1,...,φ_nを仮定とする結論と定義する。
論理的公理と公理は、仮定かつ結論と定義する。
天々城
「この変形する元の論理式を『仮定』、
変形された論理式を『結論』と定義するわけだ。
しかも推論規則を組み合わせても推論規則になる」
さトぅー
「論理式を論理式にうつす写像なんだけど、メタな言語がわかってないと無理か」
天々城
「どこかの階層で理解してもらうしかない」
エーリル
「えっと……、えっと？」
天々城
「保留で」
エーリル
「保留で」
さトぅー
「このAx1,Ax2,Ax3,⇒elの組で命題論理G0が定義された。
言い方を変えれば、この組を変えれば言語も変わるってわけね」
エーリル
「命題論理という兵器を手に入れた」
天々城
「圧倒的英知の力」
エーリル
「で、どうしゃべるの？」
さトぅー
「じゃあ証明を定義しようか」
■証明の定義
φ_1,……,φ_Nは論理式の「有限」列で、
(1) Nが1のとき、φ_1が論理的公理または公理ならφ_1は証明。
(2) Nがn+1のとき、φ_1,……,φ_nが証明で、φ_n+1が論理的公理または公理またはφ_1,……,φ_nの中からいくつかを仮定とする推論規則の結論なら証明。
さトぅー
「あと定理も定義する」
■定理|-の定義
Tを公理とする。
証明φ_1,……,φが存在するとき、T |- φ(φはTの定理)と定義する。
天々城
「命題論理以外の言語の証明と定理の定義も大体一緒だナ。
稀に例外もあるが」
エーリル
「よくわからない。例がほしい」
さトぅー
「じゃあ証明してみよう」
■thm0.0
{} |- (φ⇒φ)
-----------------
さトぅー
「まず、自分が示したい定理を書く」
エーリル
「thm0.0と{}はなに？」
さトぅー
「thm0.0は定理に名前をつけただけ。
このあと何回か使うつもりだから、全部書いてたら面倒くさいでしょ」
エーリル
「たしかに」
さトぅー
「{}は公理がなにもないってこと。
あるなら{φ}とか{(￢φ),(φ⇒ψ)}とか書く」
エーリル
「論理的公理は書かないの？」
さトぅー
「今、命題論理の言語で証明をしようとしてるじゃない？
言語で固定しっぱなしだから省略するの」
エーリル
「なるほど、わかった」
----------------
proof
1 (φ⇒((φ⇒φ)⇒φ)) [Ax1]
---------------
エーリル
「1ってなに？」
さトぅー
「証明を定義したときに、φ_1って出てきたよね」
エーリル
「あっ、論理式の列の1番目ってこと？」
さトぅー
「そうそう。行数ともいう」
エーリル
「それで1番目がAx1……。
あれ、でもこれAx1と違う論理式じゃ……」
さトぅー
「そっか。言い忘れてた。
Ax1,Ax2,Ax3,⇒elはすべての論理式で使っていいの。
だから、Ax1の論理式(φ⇒(ψ⇒φ))に出てくるψに(φ⇒φ)を代入したら1行目になってるでしょ？」
エーリル
「あー、ほんとだ」
さトぅー
「1行目は論理的公理Ax1だから証明の定義から証明になってる」
エーリル
「やりたいことがわかってきた」
------------------------
2 ((φ⇒((φ⇒φ)⇒φ))⇒((φ⇒(φ⇒φ))⇒(φ⇒φ))) [Ax2]
3 ((φ⇒(φ⇒φ))⇒(φ⇒φ)) [⇒el 1,2]
------------------------
エーリル
「[⇒el 1,2]ってなに？」
さトぅー
「1行目と2行目を仮定にして推論規則⇒elを使った。
その結論が3行目ってこと。
だから1行目から3行目も証明になってる」
エーリル
「たぶんそうだと思ってた」
-----------------------
4 (φ⇒(φ⇒φ)) [Ax1]
5 (φ⇒φ) [⇒el 4,3]
■
さトぅー
「これで証明終了」
天々城
「倒した」
エーリル
「倒した」
天々城
「今から{} |- (φ⇒φ)を倒す。
proof、戦歴。
そして倒した」
さトぅー
「なに教えてるのよ」
エーリル
「んー。考えた足跡が証明で、考えていきついた先が定理って感じる」
天々城
「実際、それしかやってないからナ。
格好つけて証明とか定理とか言ってるだけ」
エーリル
「わかる」
さトぅー
「さっき倒した倒した言ってなかった？ ねえ？」
