『現代数理論理学序説』勉強会

ぼんてんぴょん(Bontenpøn) @y_bonten

現代数理論理学序説p12、青いところはβじゃなく他の文字でも大丈夫、というのは私の持ちネタ pic.twitter.com/qUIS91ugGY

拡大

ぼんてんぴょん(Bontenpøn) @y_bonten

現代数理論理学序説、問1.2.5-2： α→(β→γ)をp、(α→β)→(α→γ)をqと略記すると、公理2はp→qと書ける。p,qの内実に関わらず 公理1から(p→q)→(δ→(p→q))、 公理2から(δ→(p→q))→((δ→p)→(δ→q))、 これらからMP2回で(δ→p)→(δ→q)を得る。p,qを書き戻せば、要求された論理式を得る。

ぼんてんぴょん(Bontenpøn) @y_bonten

ヒルベルト流の（無駄に難しいことによる）醍醐味だが、公理と推論規則から得られた定理のシェマに公理そのものの部品を放り込むような所業が楽しい。

ぼんてんぴょん(Bontenpøn) @y_bonten

ヒルベルト流の証明で補題を（派生規則でなく）含意命題として切り出してしまうと、MPを使う回数が返って増えちゃうんだな……

ぼんてんぴょん(Bontenpøn) @y_bonten

現代数理論理学序説・問題1.2.5(3)(β→γ)→((α→β)→(α→γ))、意味内容としては三段論法ですね。 公理1から(β→γ)→(α→(β→γ)) 公理2から(α→(β→γ))→((α→β)→(α→γ)) この2つから三段論法で証明すればOK……って今その三段論法を証明するんやないかーい！っていう、これがいいんですよこれが。

ぼんてんぴょん(Bontenpøn) @y_bonten

β→γをr、(α→(β→γ))をs、(α→β)→(α→γ)をtとおくと、上の2式はr→sとs→tと書ける。ここからr→tを出したい。r,s,tに対して再び公理1から(s→t)→(r→(s→t))、公理2から(r→(s→t))→((r→s)→(r→t))。今度はr→sとs→tが使えるので、MP3発でr→tが出る。r,tを書き戻せば、要求された式を得る。

ぼんてんぴょん(Bontenpøn) @y_bonten

解答例でも、まとまった式を別の文字（α1とか）で略記している。ただ、略記の選び方は紙面の節約の観点からなされていて、証明の枠組みを理解しやすいように置いてくれているかというとちょっと違う。全貌が見渡しやすいように自分で置いてみるのも良いと思う。

ぼんてんぴょん(Bontenpøn) @y_bonten

1.2.5(3)のような含意命題の形でなく派生規則としてβ→γ├(α→β)→(α→γ)を得るだけなら、単純にこのままの形でMP2発で得られるのでずいぶん楽だ。この派生規則のα,β,γとして、改めてδ,α→(β→γ),(α→β)→(α→γ)を入れると1.2.5(2)で要求された論理式の証明が得られる。

ぼんてんぴょん(Bontenpøn) @y_bonten

『現代数理論理学序説』問題1.2.5(7)注「¬¬α⊃αは¬¬(α⊃α)を省略したものではない」って、なんだこの注記は。そこまでの説明で¬と⊃の優先順位を明記していないにも関わらず、「こうではないので注意」って。直接「(¬(¬α))⊃αの略記である」と書けばいいだけの話。

ぼんてんぴょん(Bontenpøn) @y_bonten

問1.2.5(7)の証明が思いついた過程：三段論法の組み方はすでに知っているわけだから、¬¬α→●と●→αの2つが示せればよい。実のところ¬¬α⇔αのはずだから、●にもαと同値な論理式が入るはず。後者を公理Pから作る線を狙うと、((α→⊥)→α)→α（Pのβを⊥にした）、これは(¬α→α)→αにほかならず、おぉ、

ぼんてんぴょん(Bontenpøn) @y_bonten

¬α→αならαと同値だから、これを●にすればいいかも。すると前者は(¬α→⊥)→(¬α→α)になるが、これは公理Sの後件の形をしており、当てはめるなら前件は¬α→(⊥→α)になるはず。これはA:⊥→αをKで水増ししてやれば得られるはずだから一丁上がり。

ぼんてんぴょん(Bontenpøn) @y_bonten

現代数理論理学序説p13、「大雑把に言えば，直観主義命題論理は古典命題論理の公理型から公理型P（引用者注：⊥→α）を除いて得られるものです．しかし，直観主義論理では❛∧❜と❛∨❜を❛⊃❜と❛⊥❜を使って定義することはできません．」；

ぼんてんぴょん(Bontenpøn) @y_bonten

「なんで？さっきと同じように定義すればいだけじゃない？」と思ってしまうが、たぶんそういう話じゃなくて、そう定義したら直観主義論理と等価なものにならない不都合があるのだろう。ここだけをいくら読んでいても分かるはずがないので保留して進もう。

ぼんてんぴょん(Bontenpøn) @y_bonten

「論理記号❛⊥❜をもつかもたないかは本質的なことではありません．論理記号❛⊥❜についての（❛⊥❜を陽に含む）公理型をもつかもたないかが重要なのです．」；これは直観主義論理と最小論理の違いを知っていれば理解しやすい。

ぼんてんぴょん(Bontenpøn) @y_bonten

公理だと話が面倒なので推論規則で言わせてもらうと、例えばAと¬Aから⊥を導けるという規則があったとしても、肝心の「¬A」の定義が「A→⊥」なのだから、これはMPで後件がたまたま⊥だった場合に過ぎない。だから、こんな規則を足しても実質は何も変わらない。そういう話だろうと思う。

ぼんてんぴょん(Bontenpøn) @y_bonten

『現代数理論理学序説』、やっっっっとCLwの公理の正体を悟った！ KMN>1 Mは、仮定M,Nが立っているときに、「M→(N→M)（公理Kによる）とMから、N→M。さらにこれとNから、M」と推論していいが、初めから仮定にMがあるので無駄、ということか。

ぼんてんぴょん(Bontenpøn) @y_bonten

SMNR>1 MR(NR)は、α→(β→γ),(α→β),αをそれぞれM,N,Rと置き、これら３つが仮定として立っているとき、M→(N→(R→γ))（公理Sによる）から順次MPでγが得られる。同じ結論を得るためには、MとRからβ→γを、NとRからβを得ておき、β→γとβから証明することもできる、という意味。

ぼんてんぴょん(Bontenpøn) @y_bonten

つうことはCLwの推論図は、命題論理の推論図そのものを対象に推論しているということか。萌えるなぁ。

ぼんてんぴょん(Bontenpøn) @y_bonten

仮定付きの具体的な証明を、演繹定理の証明に書かれた通りのレシピで仮定なしの証明に書き換えることができなかったら、演繹定理を理解しているとは言い難いと思うのだが、ちょっと厳しすぎるのだろうか。

ぼんてんぴょん(Bontenpøn) @y_bonten

『現代数理論理学序説』問題1.2.5(3)の解答例で追加された1.2.5(8)の解答例で、α5→α4を導くところが遠回りに見える。(3)を2箇所に利用しているが、Π1のほうは不要ではないか。α6をKで(α→(β→γ))→α6に水増ししてからSで振り分ければS(KB):α5→α4が得られる。

ぼんてんぴょん(Bontenpøn) @y_bonten

ただ、解答例の方法で最後にできるS(BBS)KKにCという略号が与えられているので、なにか定石的な方法にのっとっているのかもしれない。

ぼんてんぴょん(Bontenpøn) @y_bonten

『現代数理論理学序説』問題1.2.9、まぁ何度やっても計算が合わないが、解答例と突き合わせても処理の順番が自分と異なるので照合に難航する。そもそも内側を先に計算しても外側を先にしても最終結果が同じになるんだろうかと不安になる。

ぼんてんぴょん(Bontenpøn) @y_bonten

しかし例えば S(SMNR)TU->S(MR(NR))TU->MR(NR)U(TU) S(SMNR)TU->SMNRU(TU)->MR(NR)U(TU) となるので、大丈夫なようだ。慣れてくると内側と外側を同時に処理することもできるようになる。「書き換えができる状態になったらすかさず処理する」という方針に従えば、次のように7ステップで済む。

ぼんてんぴょん(Bontenpøn) @y_bonten

S(S(KS)(S(S(KS)(S(KK)I))(KI)))(KI)xy ->S(KS)(S(S(KS)(S(KK)I))(KI))x(KIx)y ->KSx(S(S(KS)(S(KK)I))(KI)x)Iy ->S(S(KS)(S(KK)I)x(KIx))Iy ->KSx(S(KK)Ix)Iy(Iy) ->S(KKx(Ix))Iyy ->Kxy(Iy)y ->xyy

ぼんてんぴょん(Bontenpøn) @y_bonten

悟りが開けてきた。無駄にMPの多い証明をリファクタリングしている、この俺の所業を抽象化したものがコンビネータの簡約なのだ！うぉぉ！