やっぱりこの方法ギャップがあると思う!!(スコーレム公理を追加すればこの論法で行けると思うけど)

Show thread

様々な物理学の分野の中で量子力学はかなり数学的にきれいに整備されていると感じるが、比べて熱力学や電磁気学は意味不明だと思った

lean4よさそうなので早くステーブルになってほしい

lean-logic/QL/FOLの論理式は自由変項の数が型によって有限個に定まっているためこの方法で証明するのは難しい

Show thread

追加されるのが関係記号だけなら簡単な帰納法で証明できるが問題は関数記号の追加にあり、flypitchやlean-logic/FOLでは未知の関数記号を含む項を自由変項に変換して証明している

スコーレム化して完全性を証明する方法(cf. 田中 一之『計算理論と数理論理学』)がうまく行かなかったのでTait-calculusで完全性を証明してからカット除去定理を証明してHilbert styleの証明可能性との等価性を示すという方向でやっていく

Show older
mstdn.jp

Mastodon日本鯖です. よろしくお願いいたします。 (Maintained by Sujitech, LLC)