現代数理論理学序説 p.45 自然推論NJでは、論理記号'⊥'を含まない論理式αに至る正規な証明図に現れる論理式はαの部分論理式だけである これの証明のチャレンジしてみました。 正規な推論図であることの別定義 推論図が正規形であることは、以下で定義される…

終わったと同時に記事に書き起こす気力があまりなくなりましたが重要な部分だけ書きます。 「束縛変数が与えられた有限集合と重なりがないようにα変換できる」を有効に活用することでなんとか証明が完成しました。 証明の中で命題を適用する際の細かい前提条…

前回の記事の要約: (A): M →1β N, M ≡α M' ⇒ M' →1β N (B): M ▷1β N ⇒ [t/s]M →1β [t/s]N という二つの命題を証明しようとしたが(A)と(B)の証明が相互依存になってしまって、それを二つの証明の帰納法を同時に実行することで解消するという大掛かりな方法を…

二つの命題が相互依存になって、二つの証明の帰納法を同時に実行することで解消するという大掛かりな方法になってしまった。 既知とする命題 既知の命題1: λx.Q ≡α λy.Q' ⇔ Q' ≡α [y/x]Q かつ [x≡y または y ∉ FV(Q)] 既知の命題2: R' ≡α R, λy.Q' ≡α λx.Q ⇒…

補助定理1.2.34(3) 任意のラムダ項Mに対して次のようなラムダ項Nが存在する M ≡α N かつ FN(N) ∩ BV(N) = ∅ 以下の二つの命題と本の中の補助定理1.2.34(3)よりも前に登場する定理を既知とする。 主張A: BV([y/x]M) = BM(M) (y ∉ BV(M)) 主張B: [z/y][y/x]M ≡…

現代数理論理学序説は今α同値をやっています。次の(本には証明の書かれていない)定理の証明が存外手間がかかったので記しておきます。 補助定理1.2.32(2) (の⇒の部分) V(λxy.MN)に属さない任意の変数zに対してλx.M ≡α λy.N ⇒ [z/x]M ≡α [z/y]N この定理は次…

最近現代数理論理学序説を読み始めました。今日は体系CLwで遊びました。Lazy Kを触ったことがあったので、この体系にはどういう意図があるのかはなんとなくわかった上で進められました。 本に載っていない命題で、次のようなものを見つけて証明しました は許…

数学ガールゲーデル編では表現定理の証明が省略されている 体系には足し算なんて用意されていないのにたとえばどうやって三項関係を表現するんだろうと気になる。これはだいたい予想がついた。 二項関係を表現する論理式は、が属していて任意のについてが属…

最近ゲーデルの不完全性定理の証明に登場する形式的体系で遊んでます。 数学ガール ゲーデル編を読んで以来、からが導けるという推論規則がなんであるのか、を公理とするのではだめなのか気になっていました。その疑問が解決しました。任意の論理式について…