ヒルベルト・バーネイスの証明可能性条件

数理論理学において、ヒルベルト・バーネイズの証明可能性条件は、デイヴィッド・ヒルベルトとポール・バーネイズにちなんで名付けられ、算術の形式理論における形式化された証明可能性述語に対する一連の要件である (Smith 2007:224)。

これらの条件は、クルト・ゲーデルの第二不完全性定理の多くの証明で使用され、証明可能性論理の公理とも密接に関連しています。

T を、形式化された証明可能性述語Prov( n )を持つ算術の形式理論とします。これは、1つの自由数変数を持つTの式として表現されます。理論内の各式φに対して、 #(φ)をφのゲーデル数とします。ヒルベルト・バーネイスの証明可能性条件は次のとおりです。

1. Tが文φを証明する場合、T はProv(#(φ))を証明します。
2. あらゆる文φに対して、TはProv(#(φ)) → Prov(#(Prov(#(φ))))を証明する。
3. TはProv(#(φ → ψ))とProv(#(φ))がProv(#(ψ))を意味することを証明する

Prov は数の述語であり、 Prov(#(φ))の意図された解釈はφの証明をコード化する数が存在するということであるという意味において証明可能性述語であることに注意してください。 形式的には、 Provに要求されるのは上記の 3 つの条件です。

証明可能性論理のより簡潔な表記では、は「証明する」を表し、 は以下を表します。 ${\displaystyle T\vdash \varphi }$${\displaystyle T}$${\displaystyle \varphi}$${\displaystyle \Box \varphi }$${\displaystyle {\text{証明}}(\#(\varphi ))}$

1. ${\displaystyle (T\vdash \varphi )\to (T\vdash \Box \varphi )}$
2. ${\displaystyle T\vdash (\Box \phi \to \Box \Box \phi )}$
3. ${\displaystyle T\vdash (\Box (\varphi \to \psi )\to \Box \varphi \to \Box \psi )}$

ヒルベルト・バーナイスの証明可能性条件と対角補題を組み合わせると、ゲーデルの不完全性定理の両方をすぐに証明できます。実際、ゲーデルの証明の主な努力は、これらの条件（または同等の条件）と対角補題がペアノ算術に当てはまることを示すことでした。これらが確立されると、証明は簡単に形式化できます。

対角線の補題を用いると、となる式が存在します。 ${\displaystyle \rho}$${\displaystyle T\Vdash \rho \leftrightarrow \neg Prov(\#(\rho ))}$

最初の定理では、最初の条件と 3 番目の条件のみが必要です。

Tがω 整合であるという条件は、すべての式φに対して、T がProv(#(φ)) を証明する 場合、T はφ を証明するという条件によって一般化されます。これは確かにω整合Tに当てはまります。なぜなら、Prov(#(φ)) はφの証明のための数値コーディングがあることを意味し、Tがω整合であれば、すべての自然数を調べることで実際にそのような特定の数a を見つけることができ、a を使用してTにおけるφの実際の証明を構築できるからです。

T が を証明できたと仮定します。その場合、 Tには次の定理が成立します。 ${\displaystyle \rho}$

1. ${\displaystyle T\Vdash \rho }$
2. ${\displaystyle T\Vdash \neg Prov(\#(\rho ))}$（定理1の構築により）${\displaystyle \rho}$
3. ${\displaystyle T\Vdash Prov(\#(\rho ))}$（条件1と定理1による）

したがって、T はと の両方を証明します。しかし、 Tが矛盾しない場合、これは不可能であり、T はを証明しないと結論せざるを得ません。 ${\displaystyle 証明(\#(\rho ))}$${\displaystyle \neg Prov(\#(\rho ))}$${\displaystyle \rho}$

ここで、 T がを証明できたと仮定します。その場合、 Tには次の定理が成り立ちます。 ${\displaystyle \neg \rho}$

1. ${\displaystyle T\Vdash \neg \rho }$
2. ${\displaystyle T\Vdash Prov(\#(\rho ))}$（定理1の構築により）${\displaystyle \rho}$
3. ${\displaystyle T\Vdash \rho }$（ω-一貫性による）

したがって、T はと の両方を証明します。しかし、 Tが矛盾しない場合、これは不可能であり、T はを証明しないと結論せざるを得ません。 ${\displaystyle \rho}$${\displaystyle \neg \rho}$${\displaystyle \neg \rho}$

結論として、T はもも証明できません。 ${\displaystyle \rho}$${\displaystyle \neg \rho}$

Rosser のトリックを使用すると、Tがω整合的であると仮定する必要はありません。ただし、1 番目と 3 番目の証明条件が、単純な証明述語 Prov ではなく、 Rosser の証明述語Prov ^Rに対して成立することを示す必要があります。これは、すべての式φに対して、Prov ^Rが成立する場合に限り、Prov(#(φ)) が成立するという事実から導かれます。

使用される追加の条件は、T がProv ^R (#(φ))が¬Prov ^R (#(¬φ))を意味することを証明することです。この条件は、論理と非常に基本的な算術を含むすべてのTに当てはまります ( Rosser のトリック#Rosser 文で詳しく説明されています)。

Rosser のトリックを使用すると、ρ は、単純な証明可能性述語の代わりに Rosser の証明可能性述語を使用して定義されます。証明の最初の部分は、証明可能性述語が Rosser の証明可能性述語に置き換えられていることを除いて変更されません。

証明の2番目の部分ではω一貫性は使用されなくなり、次のように変更されます。

T がを証明できたと仮定します。その場合、 Tには次の定理が成立します。 ${\displaystyle \neg \rho}$

1. ${\displaystyle T\Vdash \neg \rho }$
2. ${\displaystyle T\Vdash 証明^{R}(\#(\rho ))}$（定理1の構築により）${\displaystyle \rho}$
3. ${\displaystyle T\Vdash \neg Prov^{R}(\#(\neg \rho ))}$（定理2とロッサーの証明可能性述語の定義に続く追加条件により）
4. ${\displaystyle T\Vdash 証明^{R}(\#(\neg \rho ))}$（条件1と定理1による）

したがって、T はと の両方を証明します。しかし、 Tが矛盾しない場合、これは不可能であり、T はを証明しないと結論せざるを得ません。 ${\displaystyle 証明^{R}(\#(\neg \rho ))}$${\displaystyle \neg 証明^{R}(\#(\neg \rho ))}$${\displaystyle \neg \rho}$

T が自身の一貫性を証明すると仮定します。つまり、

${\displaystyle T\Vdash \neg Prov(\#(1=0))}$。

すべての式φについて:

${\displaystyle T\Vdash \neg \varphi \rightarrow (\varphi \rightarrow (1=0))}$（否定除去により）

後者の定理に条件 1 を適用し、続いて条件 3 を繰り返し適用すると、次のことが示されます。

${\displaystyle T\Vdash Prov(\#(\neg \varphi ))\rightarrow (Prov(\#(\varphi ))\rightarrow Prov(\#(1=0)))}$

そして、T が自身の一貫性を証明すると、次のようになります。

${\displaystyle T\Vdash Prov(\#(\neg \varphi ))\rightarrow \neg Prov(\#(\varphi ))}$

これを使って、Tが一貫していないことを示します。

1. ${\displaystyle T\Vdash Prov(\#(\neg Prov(\#(\rho )))\rightarrow \neg Prov(\#(Prov(\#(\rho )))}$（Tが自身の一貫性を証明した後、）${\displaystyle \varphi =Prov(\#(\rho ))}$
2. ${\displaystyle T\Vdash \rho \rightarrow \neg Prov(\#(\rho ))}$（の構築により）${\displaystyle \rho}$
3. ${\displaystyle T\Vdash Prov(\#(\rho \rightarrow \neg Prov(\#(\rho )))}$（条件1と定理2による）
4. ${\displaystyle T\Vdash Prov(\#(\rho ))\rightarrow Prov(\#(\neg Prov(\#(\rho )))}$（条件3と定理3による）
5. ${\displaystyle T\Vdash Prov(\#(\rho ))\rightarrow \neg Prov(\#(Prov(\#(\rho )))}$（定理1と4より）
6. ${\displaystyle T\Vdash Prov(\#(\rho ))\rightarrow Prov(\#(Prov(\#(\rho )))}$（条件2による）
7. ${\displaystyle T\Vdash \neg Prov(\#(\rho ))}$（定理5と6より）
8. ${\displaystyle T\Vdash \neg Prov(\#(\rho ))\rightarrow \rho }$（の構築により）${\displaystyle \rho}$
9. ${\displaystyle T\Vdash \rho }$（定理7と8より）
10. ${\displaystyle T\Vdash Prov(\#(\rho ))}$（条件１と定理９より）

したがって、T はと の両方を証明するので、T は矛盾します。 ${\displaystyle 証明(\#(\rho ))}$${\displaystyle \neg Prov(\#(\rho ))}$

• スミス、ピーター（2007年）。ゲーデルの不完全性定理入門。ケンブリッジ大学出版局。ISBN 978-0-521-67453-9