恒真性って任意の個体領域で真となる性質の事でモデルなんて出てこないっすよ。

素朴な疑問なんですが、不完全性定理の証明に出てくる述語 Bew って
単項述語をとる述語で二階述語です。だから
∃r . Bew(r)
が恒真だけど決定不可能、
つまり恒真ということを公理系から確認するためのアルゴリズムが原理的にない
ってことですよね。
というわけで、恒真論理式≠決定可能な論理式
で公理系が完全ではない

全然関係ないですが公理系が完全ってヒルベルト空間の基底が完全系を成すというのが元だと思う。