mr_konn氏による決定性公理オフ実況

スマートコン @mr_konn

決定性公理オフなう

スマートコン @mr_konn

不法占拠なう

スマートコン @mr_konn

ざんさんと iPhone 越しにつながる会場 #ad_off

スマートコン @mr_konn

iPhone を回して画面の中のざんさんに自己紹介してる #ad_off

スマートコン @mr_konn

未来感あふれる #ad_off

スマートコン @mr_konn

まずはのうこさんの発表〜 #ad_off

スマートコン @mr_konn

私がしるぽさんのクラスメイトに激似らしい #ad_off

スマートコン @mr_konn

Skype 越しに iPhone を Web カメラにして音声・映像中継手段を確立した！！ #ad_off

スマートコン @mr_konn

「キムタク」という文字列自体はイケメンでもジャニーズに属してもいない。文字それ自身と中身を区別することがだいじ。 #ad_off

スマートコン @mr_konn

（質料代示のはなしだな #ad_off

スマートコン @mr_konn

「キムタク」の場合だとそりゃ違うよね、という感じだけど、「1」 と、何か数学的概念の "1" は違う、というのは忘れてしまいがち #ad_off

スマートコン @mr_konn

公理と呼ばれる記号列を公理へ変形するのが証明だと述べた。でも普段やっているのはそれだけではなく、仮定を置いてそこから結論を出す。背理法なら ¬φ と仮定して ⊥（矛盾）が出て来たから、¬¬φ、つまりφを結論する。 #ad_off

スマートコン @mr_konn

だから証明には二通り。公理から結論を出すのと、仮定から結論を出すのの二つの種類がある。 #ad_off

スマートコン @mr_konn

（古典論理主義者だ！殺せ！ #ad_off

スマートコン @mr_konn

（つどいでの発表のときは推論規則を全部書いた。変数条件が面倒だったのでそこだけ省略した #ad_off

スマートコン @mr_konn

形式的証明の例。Peano 算術から 1+1 = 2 をしめしてみる（ロビンソンでいいんだけど、まあ有名なのは Peano なので）。A1. ∀x¬(Sx = 0)、A2. ∀x∀y ((Sx = Sy) → (x=y))、A3. ∀x( (x + 0) = x) #ad_off

スマートコン @mr_konn

A4. ∀x∀y(x+Sy = S(x+y))。これから S0 + S0 = SS 0 を示す。 #ad_off

スマートコン @mr_konn

これは標準的な解釈のもとで 1+1 = 2の証明になる。 #ad_off

スマートコン @mr_konn

A4 -------- ∀x(S0+Sy = S(S0+y) A3 ------------------- --------- S0 + S0 = S(S0 + 0) S0+0 = S0 -------------------- S0 + S0 = SS0 #ad_off

スマートコン @mr_konn

（Twitter に無理矢理証明図を書いた #ad_off

スマートコン @mr_konn

これは意味を抜きにして完全に形式的な変形でできる。意味を考えずに、規則を組み合わせて図を書いてみて、といったら小学生でも書ける。 #ad_off

スマートコン @mr_konn

前回の発表では、「推論規則ってそれだけで実際の数学カバー出来るの？」と云われた。でも、ほかの規則も全部同じ規則から導ける。 #ad_off

スマートコン @mr_konn

例えば対偶。 φ φ→ψ ------- ψ ¬ψ ----------- ¬E ⊥ -------- ¬I ¬ψ→¬φ #ad_off

スマートコン @mr_konn

……というような発表をつどいでした。何か意見などがあれば？ #ad_off

スマートコン @mr_konn

「推論規則が取り尽せているということは、完全性のことを云ったほうがいいのでは？」 #ad_off