ω-無矛盾理論

数理論理学において、ω-無矛盾（またはオメガ-無矛盾、数値的分離とも呼ばれる）^[1] 理論とは、（統語的に）無矛盾であるだけでなく^[2]（つまり、矛盾を証明しない）直感的に矛盾する文の特定の無限の組み合わせを証明することを避ける理論（文の集合）である。この名前は、不完全性定理を証明する過程でこの概念を導入したクルト・ゲーデルに由来する。^[3]

算術の公式を理論Tの言語に翻訳することができ、その翻訳に基づいてT が自然数の基本公理を証明できる場合、理論Tは算術の言語を解釈すると言われる。

算術を解釈する T が ω 矛盾であるとは、自然数のある特性P （ Tの言語の式で定義）に対して、T がP (0)、P (1)、P (2) などを証明する（つまり、すべての標準的な自然数nに対して、T はP ( n ) が成り立つことを証明する）が、 P ( n )が成り立たない自然数nが存在することも証明する場合である。^[2] Tは、特定のnの値に対してP ( n ) が成り立たないことを証明できず、そのようなnが存在することしか証明できないため、 T内で矛盾は発生しない可能性がある。特に、そのようなnは、Tのどのモデルでも必ず非標準の整数になる（そのため、クワインはそのような理論を「数値的に非分離的」と呼んだ）。^[4]

T は、ω不整合でない場合、 ω 整合です。

_{Σ 1}健全性という、より弱いが密接に関連した性質がある。理論TがΣ ₁健全（または別の用語では1 整合）である^[5]とは、 Tで証明可能なすべての Σ ⁰ ₁文^[6]が算術Nの標準モデル（つまり、加算と乗算を含む通常の自然数の構造）で真である場合である。Tが計算の合理的なモデルを形式化できるほど十分強い場合、Σ _{1健全性は、} T がチューリングマシンC が停止することを証明するときはいつでも、C が実際に停止することを要求するのと同等である。すべての ω 整合理論は Σ ₁健全であるが、その逆は当てはまらない。

より一般的には、算術階層のより高いレベルについて類似の概念を定義できます。Γ が算術文の集合 (通常、あるnに対して Σ ⁰ _n ) である場合、理論T は、 Tで証明可能なすべての Γ 文が標準モデルで真である場合に Γ健全です。Γ がすべての算術式の集合である場合、 Γ健全性は単に (算術)健全性と呼ばれます。T の言語が算術言語のみで構成されている場合(たとえば、集合論とは対照的に)、健全なシステムとは、モデルが通常の数学的自然数の集合である集合 ω として考えることができるシステムです。一般的なTの場合は異なります。以下の ω 論理を参照してください。

Σ _n健全性には次のような計算上の解釈があります。理論によってΣ _{n −1}オラクルを使用するプログラムC が停止することが証明された場合、C は実際に停止します。

ペアノ算術理論を PA 、主張「PA は矛盾しない」を形式化する算術ステートメントを Con(PA) と書きます。Con(PA) は、「自然数n はPA における 0=1 の証明のゲーデル数ではない」という形式になります。 ^[7] ここで、PA の矛盾がないということは、PA + ¬Con(PA) の矛盾がないことを意味します。実際、PA + ¬Con(PA) が矛盾していた場合、PA だけで ¬Con(PA)→0=1 が証明され、PA における背理法によって Con(PA) が証明されます。ゲーデルの第 2 不完全性定理により、PA は矛盾することになります。

したがって、PA が矛盾しないと仮定すると、PA + ¬Con(PA) も矛盾しません。ただし、ω 矛盾ではありません。これは、任意のnに対して、PA、したがって PA + ¬Con(PA) は、n が0=1 の証明のゲーデル数ではないことを証明するためです。ただし、PA + ¬Con(PA) は、ある自然数nに対して、n がそのような証明のゲーデル数 であることを証明します(これは、¬Con(PA) の主張を直接言い換えただけです)。

この例では、公理 ¬Con(PA) は Σ ₁であるため、システム PA + ¬Con(PA) は実際には Σ ₁不健全であり、ω 矛盾しているだけではありません。

T をPA とし、各自然数nに対して公理c  ≠  n を満たすものとします。ここでcは言語に追加された新しい定数です。このとき、T は算術的には健全です ( PA の非標準モデルはすべてTのモデルに拡張できるため) が、ω 矛盾があります ( 、およびすべての数nに対してc  ≠  n であることが証明されているため)。 ${\displaystyle \exists x\,c=x}$

算術言語のみを使用して、 Σ ₁健全な ω 矛盾理論は次のように構築できます。I Σ n_をPA のサブ理論とし、帰納スキーマを Σ _n式に制限します ( n > 0の場合 )。理論I Σ _{n  + 1}は有限に公理化可能であるため、A をその唯一の公理とし、理論T  =  I Σ _n  + ¬ Aを考えます。Aは帰納スキーマのインスタンスであると仮定できます。これは次の形式を持ちます。

${\displaystyle \forall w\,[B(0,w)\land \forall x\,(B(x,w)\to B(x+1,w))\to \forall x\,B(x,w)].}$

式を

${\displaystyle \forall w\,[B(0,w)\land \forall x\,(B(x,w)\to B(x+1,w))\to B(n,w)]}$

P ( n )によって、すべての自然数nに対して、理論T ( 実際には、純粋な述語計算でさえも ) はP ( n ) を証明します。一方、T は、公理 ¬ Aと論理的に同等であるため、式を証明します。したがって、Tは ω 矛盾です。 ${\displaystyle \exists x\,\neg P(x)}$

Tが Π _{n  + 3}健全であることを示すことは可能です。実際、それは (明らかに健全な) 理論 I Σ n に対して Π n + 3 保存的です。議論はより_{複雑です (}それはI Σ _nがI Σ _{n  + 1}においてΣ _{n  + 2}反射原理を満たすことを証明することに依存します)。

ω-Con(PA) を「PA は ω 矛盾がない」という命題を形式化する算術文とします。すると、理論 PA + ¬ω-Con(PA) は不健全 (正確にはΣ _{3不健全) ですが、ω 矛盾がありません。この議論は最初の例と似ています。}ヒルベルト–バーネイズ–レーブ導出可能性条件の適切なバージョンが「証明可能性述語」ω-Prov( A ) = ¬ω-Con(PA + ¬ A ) に当てはまり、したがってゲーデルの第 2 不完全性定理の類似物を満たします。

整数が真の数学的整数である算術理論の概念は、ω-論理によって捉えられる。[ 8 ^] Tを、自然数のみを保持することを意図した単項述語記号Nと、各（標準）自然数（別々の定数、または 0、1、1+1、1+1+1 などの定数項）ごとに 1 つずつ指定された名前 0、1、2、... を含む可算言語の理論とする。T自体は、実数や集合などのより一般的なオブジェクトを参照している可能性があることに注意する。したがって、 Tのモデルでは、N ( x ) を満たすオブジェクトは、T が自然数として解釈するオブジェクトであり、そのすべてが指定された名前のいずれかで命名される必要はない。

ω-論理のシステムには、通常の一階述語論理のすべての公理と規則に加えて、指定された自由変数xを持つ各T式P ( x ) に対して、次の形式の無限ω-規則が含まれます。

推測から。${\displaystyle P(0),P(1),P(2),\ldots }$${\displaystyle \forall x\,(N(x)\to P(x))}$

つまり、理論が、指定された名前で与えられた各自然数nに対してP ( n ) を個別に主張（つまり証明）する場合、規則の無限個の前提の明白な有限の普遍量化された対応物を介して、すべての自然数に対してP を一度に集合的に主張することになります。ペアノ算術などの自然数を対象とする算術理論の場合、述語N は冗長であり、言語から省略できます。その場合、各Pに対する規則の帰結は に簡略化されます。 ${\displaystyle \forall x\,P(x)}$

Tの ω モデルとは、その定義域に自然数が含まれ、指定された名前と記号Nが標準的に、それぞれそれらの数とそれらの数だけを定義域として持つ述語として解釈される T のモデルです (したがって非標準の数は存在しません)。言語に N が存在しない場合は、Nの定義域であったはずのものがモデルの定義域である必要があります。つまり、モデルには自然数だけが含まれます。( Tの他のモデルでは、これらの記号を非標準的に解釈する場合があります。たとえば、 Nの定義域は可算である必要さえありません。) これらの要件により、ω ルールはすべての ω モデルで有効になります。省略型定理の帰結として、逆も成り立ちます。つまり、理論T がω モデルを持つのは、ω 論理で一貫している場合のみです。

ω 論理と ω 一貫性は密接な関係があります。ω 論理で一貫性のある理論は、ω 一貫性もあります (算術的にも健全です)。逆は誤りです。ω 論理での一貫性は ω 一貫性よりもはるかに強い概念だからです。ただし、次の特徴は成り立ちます。理論が ω 一貫性を持つのは、ω ルールの ネストされていない適用の下でのその閉包が一貫性がある場合のみです。

理論Tが再帰的に公理化可能である場合、ω-一貫性はクレイグ・スモリニスキーにより次のように特徴付けられる: ^[9]

が整合している場合に限り、T はω 整合です。${\displaystyle T+\mathrm {RFN} _{T}+\mathrm {Th} _{\Pi _{2}^{0}}(\mathbb {N} )}$

ここで、は算術の標準モデルで有効なすべての Π ⁰ ₂文の集合であり、はTに対する一様反射原理であり、公理 ${\displaystyle \mathrm {Th} _{\Pi _{2}^{0}}(\mathbb {N} )}$${\displaystyle \mathrm {RFN} _{T}}$

${\displaystyle \forall x\,(\mathrm {Prov} _{T}(\ulcorner \varphi ({\dot {x}})\urcorner )\to \varphi (x))}$

1 つの自由変数を持つすべての式に対して。特に、算術言語における有限公理化可能な理論Tは、 T  + PA が-健全である場合にのみ ω 整合です。 ${\displaystyle \varphi}$${\displaystyle \Sigma _{2}^{0}}$

• クルト・ゲーデル (1931)。 「非常に正式な数学と教育システム I」。Monatshefte für Mathematikで。英語に翻訳すると、「プリンキピア・マセマティカと関連システムの形式的に決定不可能な命題について」となります。