ゲーデルの完全性定理の原典証明

これは完全性定理の最も基本的な形式です。ここでは、私たちの目的に都合の良い形式にすぐに言い換えます。「すべての構造」と言う場合、関係する構造は古典的（タルスキアン）解釈Iであることを明記することが重要です。ここで、I  =  <U,F>（Uは空でない（場合によっては無限の）対象集合であり、Fは解釈された記号体系の式からUへの関数の集合です）。[対照的に、いわゆる「自由論理」では、Uは空集合である可能性があります。自由論理の詳細については、カレル・ランバートの研究を参照してください。]

「φは反駁可能である」とは、定義上、「ε φは証明可能である」ことを意味します。

定理1が成り立ち、φがどの構造においても充足可能でない場合、¬φはすべての構造において有効であり、したがって証明可能である。ゆえにφは反駁可能であり、定理2が成り立つ。一方、定理2が成り立ち、φがすべての構造において有効である場合、¬φはどの構造においても充足可能でなく、したがって反駁可能である。このとき、¬¬φは証明可能であり、φも証明可能である。したがって定理1が成り立つ。

定理 2の証明は、 「 φ は反駁可能か充足可能であるかのいずれかである」ことを証明する必要があるすべての式 φ のクラスを順次制限することによって行います。最初は、このことを私たちの言語で可能なすべての式 φ について証明する必要があります。しかし、すべての式 φ に対して、より制限された式クラスCから取られた式 ψ が存在し、「ψは反駁可能か充足可能であるかのいずれかである」→「φは反駁可能か充足可能であるかのいずれかである」と仮定します。すると、この主張 (前の文で表現) が証明されれば、クラスCに属する φ についてのみ「 φは反駁可能か充足可能であるかのいずれかである」を証明すれば十分です。 φがψと証明可能かつ同等である場合（すなわち、( φ≡ψ )が証明可能である場合）、確かに「ψは反駁可能か充足可能である」→「φは反駁可能か充足可能である」ということになります（これを示すには健全性定理が必要です）。  

任意の式を、関数記号や定数記号を用いない式に書き換えるための標準的な手法は存在するが、その代償として追加の量化子を導入する必要がある。したがって、ここではすべての式がそのような記号を含まないものと仮定する。ゲーデルの論文では、そもそも関数記号や定数記号を持たない一階述語論理が用いられている。

次に、関数記号や定数記号を使用しない一般的な式φを考え、プレネックス形式定理を適用して、 φ ≡ ψとなるような正規形の式ψを見つけます( ψが正規形であるということは、 ψに含まれる量化子があれば、それらがすべてψの先頭にあることを意味します)。したがって、正規形の式φに対して定理 2 を証明すれば十分です。  

次に、 φからすべての自由変数を存在量化することによって削除します。たとえば、x ₁ ... x _nがφで自由である場合、${\displaystyle \psi =\exists x_{1}\cdots \exists x_{n}\varphi }$ψが構造Mで充足可能であるならば、確かにφも充足可能であり、ψが反駁可能であるならば、${\displaystyle \neg \psi =\forall x_{1}\cdots \forall x_{n}\neg \varphi }$は証明可能であり、¬ φも証明可能であるため、φは反駁可能である。φを文、つまり自由変数のない式に限定できることがわかる。

最後に、技術的な便宜上、φの接頭辞(つまり、 φの先頭にある量化子列で、これは正規形である) が全称量化子で始まり、存在量化子で終わるようにしたい。一般的なφ (既に証明した制約に従う) に対してこれを実現するために、 φで使用されていない1 項の関係記号Fと、2 つの新しい変数yとzを用意する。φ = (P)Φ の場合、( P ) はφの接頭辞、Φ は行列( φの残りの量化子を含まない部分) を表す。${\displaystyle \psi =\forall y(P)\exists z(\Phi \wedge [F(y)\vee \neg F(z)])}$。 以来${\displaystyle \forall y\exists z(F(y)\vee \neg F(z))}$明らかに証明可能であり、${\displaystyle \varphi =\psi }$証明可能である。

我々の一般的な式 φ は、正規形においては文であり、その接頭辞は全称量化子で始まり、存在量化子で終わります。このようなすべての式のクラスをRと呼びましょう。我々は、 Rに含まれるすべての式が反駁可能か充足可能であることを証明しなければなりません。式 φ が与えられたとき、我々は同じ種類の量化子の文字列をブロックにまとめます。

${\displaystyle \varphi =(\forall x_{1}\cdots \forall x_{k_{1}})(\exists x_{k_{1}+1}\cdots \exists x_{k_{2}})\cdots (\forall x_{k_{n-2}+1}\cdots \forall x_{k_{n-1}})(\exists x_{k_{n-1}+1}\cdots \exists x_{k_{n}})(\Phi )}$

我々は、${\displaystyle \varphi }$上記のように存在量化子ブロックで区切られた全称量化子ブロックの数を接頭辞とする。${\displaystyle \varphi }$ゲーデルがレーヴェンハイム＝スコーレムの定理のスコーレムの証明から応用した以下の補題により、一般的な公式の複雑さを大幅に軽減することができる。${\displaystyle \varphi }$以下の定理を証明する必要があります。

補題。k  ≥  1とする。次数kのRのすべての論理式が反駁可能または充足可能であるならば、次数k + 1のRのすべての論理式も同様である。  

コメント： k + 1 次式の式φを次のように考えます。  ${\displaystyle \varphi =(\forall x)(\exists y)(\forall u)(\exists v)(P)\psi }$、 どこ${\displaystyle (P)\psi }$残りは${\displaystyle \varphi }$（したがって次数はk  −  1 です）。φは、すべての x に対して、...（何か）となるような ay が存在すると述べています。すべての x に対して、yが（何か）を真にするために必要なものである場合に限りQ ′（x、y）が真となるような述語Q' があればよかったでしょう。そうすれば、φと同等の次数kの式を書くことができました。${\displaystyle (\forall x')(\forall x)(\forall y)(\forall u)(\exists v)(\exists y')(P)Q'(x',y')\wedge (Q'(x,y)\rightarrow \psi )}$この式は、すべての x に対して、Q'(x,y) を満たす ay が存在するならば、（何か）が成り立つと述べているため、確かにφと同等です。さらに、すべての x' に対して、Q'(x',y') を満たす y' が存在するため、そのような ay が存在することはわかっています。したがって、 φ はこの式から導かれます。また、この式が偽であれば、 φ も偽であることを示すのは簡単です。残念ながら、一般にそのような述語 Q' は存在しません。しかし、この考え方は、次の補題の証明の基礎として理解できます。

証明。φを次数k  + 1の式とすると 、次のように書ける。

${\displaystyle \varphi =(\forall x)(\exists y)(\forall u)(\exists v)(P)\psi }$

ここで(P)は接頭辞の残りの部分である${\displaystyle \varphi }$（したがって次数はk  – 1である ）${\displaystyle \psi }$は量化子を含まない行列です${\displaystyle \varphi }$ここでx、y、u、vは単一の変数ではなく変数のタプルを表します。例:${\displaystyle (\forall x)}$実際には ${\displaystyle \forall x_{1}\forall x_{2}\cdots \forall x_{n}}$どこ${\displaystyle x_{1}\ldots x_{n}}$それらはいくつかの異なる変数である。

ここで、x'とy'をそれぞれxとyと同じ長さの、これまで使用されていなかった変数のタプルとし、Qをxとyの長さの合計と同じ数の引数を取る、これまで使用されていなかった関係記号とする。式を考える。

${\displaystyle \Phi =(\forall x')(\exists y')Q(x',y')\wedge (\forall x)(\forall y)(Q(x,y)\rightarrow (\forall u)(\exists v)(P)\psi )}$

明らかに、${\displaystyle \Phi \rightarrow \varphi }$証明可能である。

さて、量化子の列は${\displaystyle (\forall u)(\exists v)(P)}$xまたはyの変数を含まない場合、以下の等価性は、使用している形式主義の助けを借りて容易に証明できます。

${\displaystyle (Q(x,y)\rightarrow (\forall u)(\exists v)(P)\psi )\equiv (\forall u)(\exists v)(P)(Q(x,y)\rightarrow \psi )}$

そして、これら2つの式は等価であるため、Φの中で最初の式を2番目の式に置き換えると、Φ≡Φ'となる式Φ'が得られます。

${\displaystyle \Phi '=(\forall x')(\exists y')Q(x',y')\wedge (\forall x)(\forall y)(\forall u)(\exists v)(P)(Q(x,y)\rightarrow \psi )}$

Φ' は次の形式になります${\displaystyle (S)\rho \wedge (S')\rho '}$ここで、(S)と(S')は量化子文字列であり、ρとρ'は量化子を含まない。さらに、 (S)の変数はρ'には含まれず、(S')の変数はρには含まれない。このような条件下では、次の形式のすべての式が成り立つ。${\displaystyle (T)(\rho \wedge \rho ')}$ここで、(T)は (S) と (S') に含まれるすべての量化子を任意の順序で交互に並べた量化子の列であり、(S) と (S') 内の相​​対的な順序は維持される。これは元の式 Φ' と等価である (これは、私たちが依拠する一階述語論理のもう 1 つの基本的な結果である)。すなわち、Ψ を次のように構成する。

${\displaystyle \Psi =(\forall x')(\forall x)(\forall y)(\forall u)(\exists y')(\exists v)(P)Q(x',y')\wedge (Q(x,y)\rightarrow \psi )}$

そして私たちは${\displaystyle \Phi '\equiv \Psi }$。

今${\displaystyle \Psi }$これは次数kの式であり、したがって仮定により反証可能または充足可能である。${\displaystyle \Psi }$構造Mで充足可能であることを考慮すると、${\displaystyle \Psi \equiv \Phi '\equiv \Phi \wedge \Phi \rightarrow \varphi }$我々は、${\displaystyle \varphi }$も満たされる。${\displaystyle \Psi }$反証可能であれば、${\displaystyle \Phi }$これはそれと同等です。したがって${\displaystyle \neg \Phi }$証明可能です。これで、証明可能な式の中の Q のすべての出現箇所を置き換えることができます。${\displaystyle \neg \Phi }$同じ変数に依存する別の式によって、証明可能な式が得られます。（これは一階述語論理のもう一つの基本的な結果です。論理計算に採用された特定の形式によっては、ゲーデルの論文にあるように、「関数置換」推論規則の単純な適用と見なすこともできますし、形式的な証明を考慮することによって証明することもできます。${\displaystyle \neg \Phi }$（ただし、その中のQのすべての出現箇所を、同じ自由変数を持つ別の式に置き換え、形式的証明におけるすべての論理公理は置換後も論理公理のままであり、すべての推論規則は依然として同じように適用されることに注意する。）

この場合、Q(x',y')を置き換えます。${\displaystyle \neg \Phi }$式を用いて${\displaystyle (\forall u)(\exists v)(P)\psi (x,y\mid x',y')}$ここで (x,y  |  x',y') は、ψ の代わりに、x と y を x' と y' に置き換えた別の式を書いていることを意味します。Q(x,y) は単純に次のように置き換えられます。${\displaystyle (\forall u)(\exists v)(P)\psi }$。

${\displaystyle \neg \Phi }$そして、

${\displaystyle \neg ((\forall x')(\exists y')(\forall u)(\exists v)(P)\psi (x,y\mid x',y')\wedge (\forall x)(\forall y)((\forall u)(\exists v)(P)\psi \rightarrow (\forall u)(\exists v)(P)\psi ))}$

そしてこの公式は証明可能である。なぜなら、否定の下の部分と、${\displaystyle \wedge }$符号は明らかに証明可能であり、否定の下の部分と${\displaystyle \wedge }$符号は明らかにφで、 xとyをx'とy'に置き換えるだけで、次のことがわかります。${\displaystyle \neg \varphi }$は証明可能であり、φ は反証可能である。φ が充足可能か反証可能であるかのどちらかであることを証明したので、これで補題の証明は完了する。

使用できなかったことに注意してください${\displaystyle (\forall u)(\exists v)(P)\psi (x,y\mid x',y')}$最初から Q(x',y') の代わりに、${\displaystyle \Psi }$その場合、それは整形式な式とは言えなかったでしょう。これが、証明の前のコメントに示されている議論を安易に適用できない理由です。

上記の補題が示すように、次数1のRの式φについてのみ定理を証明すればよい。Rの式には自由変数がなく、定数記号も使用しないため、φは次数0にはなり得ない。したがって、式φの一般形は次のようになる。

${\displaystyle (\forall x_{1}\ldots x_{k})(\exists y_{1}\ldots y_{m})\varphi (x_{1}\ldots x_{k},y_{1}\ldots y_{m}).}$

ここで、自然数のk組の順序を次のように定義します。${\displaystyle (x_{1}\ldots x_{k})<(y_{1}\ldots y_{k})}$どちらかの場合に保持する必要があります${\displaystyle \Sigma _{k}(x_{1}\ldots x_{k})<\Sigma _{k}(y_{1}\ldots y_{k})}$、 または${\displaystyle \Sigma _{k}(x_{1}\ldots x_{k})=\Sigma _{k}(y_{1}\ldots y_{k})}$、 そして ${\displaystyle (x_{1}\ldots x_{k})}$先行する${\displaystyle (y_{1}...y_{k})}$辞書順。[ここに${\displaystyle \Sigma _{k}(x_{1}\ldots x_{k})}$はタプルの項の合計を表します。] この順序で n 番目のタプルを で表します。${\displaystyle (a_{1}^{n}\ldots a_{k}^{n})}$。

数式を設定する${\displaystyle B_{n}}$として${\displaystyle \varphi (z_{a_{1}^{n}}\ldots z_{a_{k}^{n}},z_{(n-1)m+2},z_{(n-1)m+3}\ldots z_{nm+1})}$.次に${\displaystyle D_{n}}$として

${\displaystyle (\exists z_{1}\ldots z_{nm+1})(B_{1}\wedge B_{2}\wedge \cdots \wedge B_{n}).}$

補題：すべてのnに対して、${\displaystyle \varphi \rightarrow D_{n}}$。

証明： nに関する帰納法により、${\displaystyle D_{n}\Leftarrow D_{n-1}\wedge (\forall z_{1}\ldots z_{(n-1)m+1})(\exists z_{(n-1)m+2}\ldots z_{nm+1})B_{n}\Leftarrow D_{n-1}\wedge (\forall z_{a_{1}^{n}}\ldots z_{a_{k}^{n}})(\exists y_{1}\ldots y_{m})\varphi (z_{a_{1}^{n}}\ldots z_{a_{k}^{n}},y_{1}\ldots y_{m})}$ここで、後者の含意は変数置換によって成り立つ。なぜなら、タプルの順序は次のようになっているからである。${\displaystyle (\forall k)(a_{1}^{n}\ldots a_{k}^{n})<(n-1)m+2}$しかし、最後の式は以下と同等です。${\displaystyle D_{n-1}\wedge }$φ。

基本ケースでは、${\displaystyle D_{1}\equiv (\exists z_{1}\ldots z_{m+1})\varphi (z_{a_{1}^{1}}\ldots z_{a_{k}^{1}},z_{2},z_{3}\ldots z_{m+1})\equiv (\exists z_{1}\ldots z_{m+1})\varphi (z_{1}\ldots z_{1},z_{2},z_{3}\ldots z_{m+1})}$これは明らかにφの系でもある。したがって、補題は証明された。

今もし${\displaystyle D_{n}}$あるnに対して反証可能であるならば、φ も反証可能である。一方、${\displaystyle D_{n}}$は任意のnに対して反駁できない。すると、各nに対して、異なる部分命題に真偽値を割り当てる何らかの方法が存在する。${\displaystyle E_{h}}$（初登場順に並べると）${\displaystyle D_{n}}$（ここで「distinct」とは、異なる述語、または異なる束縛変数のいずれかを意味します）${\displaystyle B_{k}}$、したがって${\displaystyle D_{n}}$各命題がこのように評価されると、真となる。これは、基礎となる命題論理の完全性から導かれる。

これから真理値の割り当てが${\displaystyle E_{h}}$そうすればすべてが${\displaystyle D_{n}}$真実となるでしょう:${\displaystyle E_{h}}$すべての${\displaystyle D_{n}}$; 我々は、一種の「多数決」によって、それらへの一般的な割り当てを帰納的に定義します。割り当ては無限に存在するため（それぞれに1つずつ）${\displaystyle D_{n}}$）影響する${\displaystyle E_{1}}$無限に多くのものを作る${\displaystyle E_{1}}$真であるか、無限に多くのものが偽であり、有限に多くのものが真である。前者の場合、我々は${\displaystyle E_{1}}$一般的に真である。後者では、一般的に偽であるとみなす。すると、無限に多くのnから、${\displaystyle E_{1}}$を通して${\displaystyle E_{h-1}}$一般的な割り当てと同じ真理値が割り当てられる場合、一般的な割り当てを選択します。${\displaystyle E_{h}}$同様に。

この一般的な課題は、${\displaystyle B_{k}}$そして${\displaystyle D_{k}}$真実であるならば、${\displaystyle B_{k}}$一般的な割り当ての下では偽であった、${\displaystyle D_{n}}$n > kの場合にも偽となる。しかし、これは一般の有限集合の場合に矛盾する。${\displaystyle E_{h}}$掲載されている課題${\displaystyle D_{k}}$割り当てを行うnは無限に存在する${\displaystyle D_{n}}$真は一般的な割り当てと一致します。

この一般的な割り当てから、${\displaystyle D_{k}}$確かに、φ を真にする言語の述語の解釈を構築します。モデルの世界は自然数になります。各 i 項述語${\displaystyle \Psi }$自然界においては真実であるべきである${\displaystyle (u_{1}\ldots u_{i})}$まさにその命題が${\displaystyle \Psi (z_{u_{1}}\ldots z_{u_{i}})}$は、一般的な割り当てでは真であるか、または割り当てられていない（なぜなら、それはどの割り当てにも現れないからである）。${\displaystyle D_{k}}$)

このモデルでは、各式は${\displaystyle (\exists y_{1}\ldots y_{m})\varphi (a_{1}^{n}\ldots a_{k}^{n},y_{1}...y_{m})}$は構成上真である。しかし、これはモデルにおいてφ自体が真であることを意味する。なぜなら、${\displaystyle a^{n}}$φは自然数のk組のあらゆる可能な組み合わせを範囲とする。したがって、φは充足可能であり、これで完了である。

ゲーデルは、拡張言語において、等号述語を含む式を等号述語を含まない式に還元した。彼の方法は、等号述語を含む式φを、次の式に置き換えることを含む。

${\displaystyle (\forall x)Eq(x,x)\wedge (\forall x,y,z)[Eq(x,y)\rightarrow (Eq(x,z)\rightarrow Eq(y,z))]}$${\displaystyle \wedge (\forall x,y,z)[Eq(x,y)\rightarrow (Eq(z,x)\rightarrow Eq(z,y))]}$

${\displaystyle \wedge }$

${\displaystyle (\forall x_{1}\ldots x_{k},y_{1}\ldots x_{k})[(Eq(x_{1},y_{1})\wedge \cdots \wedge Eq(x_{k},y_{k}))\rightarrow (A(x_{1}\ldots x_{k})\equiv A(y_{1}\ldots y_{k}))]}$

${\displaystyle \wedge \cdots \wedge }$

${\displaystyle (\forall x_{1}\ldots x_{m},y_{1}\ldots x_{m})[(Eq(x_{1},y_{1})\wedge \cdots \wedge Eq(x_{m},y_{m}))\rightarrow (Z(x_{1}\ldots x_{m})\equiv Z(y_{1}\ldots y_{m}))]}$

${\displaystyle \wedge }$

${\displaystyle \varphi '.}$

ここ${\displaystyle A\ldots Z}$φ に現れる述語を表す (${\displaystyle k\ldots m}$φ' は、式 φ のすべての等号を新しい述語Eqに置き換えた式です。この新しい式が反証可能であれば、元の φ も反証可能でした。充足可能性についても同様で、新しい式の充足モデルをEqを表す同値関係で割った商を取ることができます。この商は他の述語に関して適切に定義されており、したがって元の式 φ を満たします。

ゲーデルは、可算無限個の論理式の集合がある場合も考察した。上記と同じ還元法を用いることで、各論理式が次数 1 であり、等号の使用を含まない場合のみを考察することができた。可算個の論理式の集合の場合、${\displaystyle \varphi ^{i}}$次数1の場合、次のように定義できます。${\displaystyle B_{k}^{i}}$上記のように定義し、次に定義する。${\displaystyle D_{k}}$閉鎖する${\displaystyle B_{1}^{1}\ldots B_{k}^{1},\ldots ,B_{1}^{k}\ldots B_{k}^{k}}$残りの証明は以前と同様に進んだ。

数えきれないほど多くの数式が存在する場合、選択公理（または少なくともその弱形式）が必要となる。完全な選択公理を用いることで、数式を整列させ、超限帰納法を用いながらも、可算の場合と同じ議論で非可算の場合も証明できる。この場合の完全性定理が、選択公理の弱形式であるブール素イデアル定理と同等であることを証明するために、他の手法も用いることができる。