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

スマートコン @mr_konn

述語論理の完全性がわからないというはなし #ad_off

スマートコン @mr_konn

Forcing と ⊨ を書き間違えていたしるぽさん #ad_off

スマートコン @mr_konn

「述語論理の完全性定理と、推論規則が妥当であることの関係性がわからない」 #ad_off

スマートコン @mr_konn

しるぽさんの説明。「⊨」は結合子（∀ ∨ ∧ など）の意味だけから真だと云えること。完全性定理は、「⊢ ⇔ ⊨ 」ということで、意味だけの真と形式での真が一致するということ。だから正当化される。 #ad_off

スマートコン @mr_konn

「意味論の話もしないと、形式と意味の区別の意味がないのではないか？真偽値くらいは書いてもよかったのでは」 #ad_off

スマートコン @mr_konn

「初心者向けこそ厳密性が必要では？」 #ad_off

スマートコン @mr_konn

「A = B から A + C = B + C みたいなことは、『なんでそこがそうなるの？』と初心者は躓いちゃったりするので、ちゃんと説明したほうがいいのでは」 #ad_off

スマートコン @mr_konn

「どこにも書いてないじゃないか！？と思うひともいる」 #ad_off

スマートコン @mr_konn

「そもそも証明から意味を抜き取る意味ってあるの？」 #ad_off

スマートコン @mr_konn

s/証明/証明や公理系/ #ad_off

スマートコン @mr_konn

「シンタックスとセマンティクスが区別出来ていない人は『こんなん自明だろ』ってやっちゃうから教育的意味はある」 #ad_off

スマートコン @mr_konn

「S0 を標準的に解釈すると 1 っていったけど、1 を S0 のことだと思えばいいのでは？」 #ad_off

スマートコン @mr_konn

「理論とは」みたいな話をしている #ad_off

スマートコン @mr_konn

宮刑〜 #ad_off

スマートコン @mr_konn

宮刑じゃねーよ休憩だよ…… #ad_off

スマートコン @mr_konn

次はしるぽさん〜 #ad_off

スマートコン @mr_konn

題「無限と有限の《弁証法（ディアレクティーク）》」 #ad_off

スマートコン @mr_konn

ゲーデルは何をやったかっていうと、・完全性定理 ・不完全性定理 ・L だろう。さらに、知る人ぞ知る「・T によるディアレクティカ解釈」がある！ #ad_off

スマートコン @mr_konn

なんで知るひとぞ知るのかというと、兎に角わかりづらい！何で提案したのかという哲学的動機も話す！（衆目の一致するところでは失敗 #ad_off

スマートコン @mr_konn

「System F って知ってますか？Girard っていういけすかないロジシャンが提案したんですけど」 #ad_off

スマートコン @mr_konn

ディアレクティカ解釈は兎に角複雑なので細かい証明はしません！ #ad_off

スマートコン @mr_konn

ディアレクティカとは何なのか？ペアノ算術の公理を、ハイティング算術に翻訳して、さらに T に翻訳する。PA の定理は HA でも定理になって、T でも定理になる。 #ad_off

スマートコン @mr_konn

そこから、 T の無矛盾性がいえれば、PA の無矛盾がわかる #ad_off

スマートコン @mr_konn

「T ってなに？」「簡単にいうと高階の原始帰納的関数（PRA）。」 #ad_off

スマートコン @mr_konn

ハイティング算術（HA）っていうのは、ペアノ算術（PA）の直観主義版。公理としては同じで、ただ、乗ってる論理がちがう。 #ad_off