Manual of First Order Theory Entailment

[SnO2WMaN]

#554 #698 などでも時たま困っているが，1階理論の証明 T ⊢ φ 上の操作や規則を一覧化したマニュアルを実際に動くサンプルコード付きで置いてあると個人的には非常に助かるし，今後もしコントリビューターが増えたときにも良いと思う．

[iehality]

Bootstrapping/RosserProvability.lean が参考になるかもしれないが，FirstOrder においては基本的に syntactic な操作で証明を行うことを想定していない．なので LO.FirstOrder.Arithmetic.provable_of_models を使うこと以上のことは言えないと思う．

[SnO2WMaN]

これは単に補題が現状揃っていないからなのか，本質的に現在の実装では技術的に困難なのかのどっちだろうか？
個人的には，少なくとも論理レベルの量化子の適当な操作とか $\forall$ 導入の操作とかを毎回モデルに立ち返ってやるよりも形式的に出来たほうが実用上は良さそうな気もする．

[iehality]

前者で，モデル論的にやるより syntactic にやるほうが楽なケースに（私が）遭遇していないからと言っていいと思う（しかし本当に syntactic な推論が必要なことはあるんだろうか？等号記号がなかったり直観主義論理だったりするならばそうだろうが，1. 通常の算術の操作は基本的に意味論でやる. 2. 最後に構文論に翻訳する，とするのが一番良いと思う）．

[iehality]

純粋に syntactic な証明は G2 の証明の際に不可欠だったので取り組んだが，非現実的に面倒，という経験則があります．cf.
https://github.com/FormalizedFormalLogic/Foundation/blob/master/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition/EquationalTheory.lean