ω整合理論

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

理論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のどのモデルにおいても必然的に非標準整数である(クワインは、このような理論を「数値的に分離不可能」と呼んだ)。^{[ 5 ]}

Tは、ω-矛盾しない場合にω-矛盾しないという。

_{Σ 1 -健全}性には、より弱いが密接に関連する性質がある。理論Tは、Tで証明可能なすべての Σ 0 1 -文 [注 1] が算術の標準モデル N (つまり、加算と乗算を備えた通常の自然数の構造) で真である場合に、^Σ ₁ -^{健全(または別}の^用語では 1 -無矛盾) [ 6 ] である。T が計算の妥当なモデルを形式化するのに十分強い場合_、 Σ 1 -^健全性は、T_がチューリングマシンCが停止することを証明するときはいつでも、C が実際に停止するという要求と同等である。すべての ω -無矛盾理論は Σ ₁ -健全であるが、その逆は成り立たない。

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

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

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

ω論理体系は、通常の1階述語論理のすべての公理と規則に加え、指定された自由変数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が再帰的に公理化可能であれば、ω-一貫性はCraig Smoryńskiにより次のように特徴付けられます。^{[ 8 ]}

Tがω整合的であるのは、以下の条件を満たす場合のみです。${\displaystyle T+\mathrm {RFN} _{T}+\mathrm {Th} _{\Pi _{2}^{0}}(\mathbb {N} )}$一貫性がある。

ここ、${\displaystyle \mathrm {Th} _{\Pi _{2}^{0}}(\mathbb {N} )}$は、算術の標準モデルにおいて有効なすべての^Π ₀ -文の集合であり、$\displaystyle \mathrm {RFN} _{T}}$Tの一様反射原理は、以下の公理から成ります。

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

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

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