Σ⊢A⇔Σ⊨A
右向きが健全性、左向きが完全性
形式的に導かれたAが恒に実際に正しい意味になっているとき、その形式的な定義は健全である。Bという意味が恒に正しいのであれば形式的にBであると導かれるとき、その形式体系は完全である。
言語Lで素数を定義したうえで、意味論的真理である「最大の素数は存在しない」という意味を導くことができなければLで表されるその論理は完全ではない。導くのに公理が足りないとなると最初から素数を定義できてなかった、言語Lで再現できてなかったという話になる。
「最大の素数は存在しない」を意味論的真理として話を進めたが、これが本当に我々がイメージする素数に関するプラトニックな真理であるかを形式的に確かめるすべは存在しない。最悪素数のイメージ自体がただの幻想かもしれない。意味論的な真理ではあってもなにか自然数論の超準的な解釈を必要とするかもしれない。いったい何が直観に沿うのかは分からないし、直観主義を持ち込むと1階述語論理が必ずしも完全でなかったりして話がこじれる。ここではあくまで形式的な議論のみを扱う、すなわち、意味が直観に沿うかどうかは気にしない。1階の言語による表現が必ず直観的イメージに沿わない意味を持ちうるというのは歴史上の大発見であった、かもしれない。
Σを有限個の命題論理式の集合として、Σ⊨φであるとき、Σに含まれる論理式をすべて論理積でつなげたものをψとしψ→φがトートロジーとなるため、モダスポーネンスよりφを導出することができ、完全性が成り立つことがわかる。問題はΣが無数の命題論理式を含むなり量化子を含むなりで始めてφが成り立つ場合が存在するか、である。たとえばペアノの公理から後者の存在を除き、0の後者が存在する、1の後者が存在する、2の後者が存在する、・・・という無数の公理を追加したうえで、「すべての自然数には後者が存在する」が導出できるか、論理的帰結となっているか、など。
命題論理の完全性とコンパクト性[]
字母
命題変数 A_1,A_2,A_3,...
論理演算子 ￢,∧,∨,→
括弧 (,)
命題変数そのもの A_i (i=1,2,3,...) は命題論理式である。
任意の文字列B,Cが命題論理式であれば、￢B,B∧C,B∨C,B→Cも命題論理式である。
いくつかの命題論理式の集合Σを理論とする。
真理値の意味の（形式的な）定義
真理値割り当て
公理
トートロジー
推論規則
BとB→CからCを推論する。
証明列
φ_0,φ_1,φ_2,...∈Seq
各φ_iにつき、φ_i∈Σまたはあるj<i,k<iが存在し、φ_j∈Seqかつφ_k=(φ_j→φ_i)かつφ_k∈Seq
健全性は再帰的に証明
完全性の証明
Σを無矛盾な理論とし、Σ⊬Bと仮定する。すべての命題論理式をB_1,B_2,B_3,...とする。 Σ∪{￢B}=Σ_1とし、Σ_{n+1}=Σ_n⊢￢B_nであればΣ_n∪{￢B_n}、そうでなければΣ_n∪{B_n} Σ^*=lim_{k→∞}Σ_k
V(B_i)をB_i∈Σ^*であればT、そうでなければFをかえす関数とする。Vが真理値割り当てであることを証明する。
よってΣを充足する任意の真理値割り当てがAを充足するわけでもないことを証明。よってΣ⊭A
完全性の証明と言うより真理値割り当ての存在と完全性が同値であることの証明ではないか、完全性の証明というには循環論法になってないかという個人的な感想。