palalansoukî @palalansouki@mstdn.jp

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

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

https://youtu.be/yq4KvIk0nFQ

https://youtu.be/ugY9CQeeNaA

https://youtu.be/xO7RgSMeG3A

https://youtu.be/u0tmXSnWClY

https://youtu.be/svFOnjjDRF0

おもしろ小説読んでる

https://youtu.be/neHyHLxwBxg

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

https://youtu.be/CSff5XkOUys

https://youtu.be/lU9eaQHMLU4

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

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

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

https://youtu.be/RscXoTm75n8

今なにしてる？