2階算術

数理論理学において、第二階算術は、自然数とその部分集合を形式化する公理体系の集合である。これは、数学のすべてではないが、多くの数学の 基礎として公理的集合論に代わるものである。

3次パラメータを含む2次演算の前身は、デイヴィッド・ヒルベルトとポール・バーネイズの著書『数学の基礎』で紹介されました。^{[1] 2次演算の標準的な公理化は}Z ₂で表されます。

2 階算術には 1 階算術であるペアノ算術が含まれますが、これよりもかなり強力です。ペアノ算術とは異なり、2 階算術では自然数の集合だけでなく、数自体の量化が可能です。実数はよく知られた方法で自然数の (無限の) 集合として表現できるため、また 2 階算術ではそのような集合の量化が可能であるため、 2 階算術で実数を形式化することができます。このため、2 階算術は「解析」と呼ばれることもあります。^[2]

2 階算術は、すべての要素が自然数または自然数の集合である集合論の弱いバージョンと見ることもできます。ツェルメロ-フランケル集合論よりもはるかに弱いですが、2 階算術では、その言語で表現可能な古典数学の結果を基本的にすべて証明できます。

2 階算術の部分系は、各公理が完全な 2 階算術 (Z ₂ )の定理である 2 階算術の言語による理論です。このような部分系は、逆数学(さまざまな強度の特定の弱い部分系で古典数学のどの程度を導出できるかを調査する研究プログラム) に不可欠です。中核となる数学の多くは、これらの弱い部分系で形式化できます。これらの弱い部分系のいくつかは、以下で定義されています。逆数学は、古典数学が非構成的である範囲と方法も明らかにします。

2 階算術の言語は2 種類に分類されます。第 1 の種類の項、特に変数は、通常小文字で表され、自然数として解釈されることを意図した個体で構成されます。もう 1 つの種類の変数は、「集合変数」、「クラス変数」、または「述語」とも呼ばれ、通常大文字で表されます。これらは個体のクラス/述語/プロパティを参照するため、自然数の集合と考えることができます。個体と集合変数は両方とも、普遍的または存在的に量化できます。束縛集合変数のない式(つまり、集合変数に対する量指定子のない式) は算術式と呼ばれます。算術式には、自由集合変数と束縛個体変数が含まれる場合があります。

個々の項は、定数 0、単項関数S (後継関数)、および二項演算 + と(加算と乗算) から形成されます。後継関数は、入力に 1 を加算します。関係 = (等号) と < (自然数の比較) は 2 つの個体を関連付けますが、関係 ∈ (メンバーシップ) は個体と集合 (またはクラス) を関連付けます。したがって、表記法では、2 階算術の言語はシグネチャ によって表されます。 ${\displaystyle \cdot}$${\displaystyle {\mathcal {L}}=\{0,S,+,\cdot ,=,<,\in \}}$

たとえば、は算術的な 2 次算術の整形式式であり、 1 つの自由集合変数Xと 1 つの束縛個別変数nを持ちます(ただし、算術式に必要な束縛集合変数はありません)。一方、は算術的ではない整形式式であり、 1 つの束縛集合変数Xと 1 つの束縛個別変数n を持ちます。 ${\displaystyle \forall n(n\in X\rightarrow Sn\in X)}$${\displaystyle \exists X\forall n(n\in X\leftrightarrow n<SSSSSS0\cdot SSSSSSS0)}$

量指定子にはいくつかの異なる解釈が可能である。2階算術を2階論理の完全な意味論を用いて研究する場合、集合量指定子は個々の変数の範囲のすべての部分集合にわたる。2階算術を1階論理の意味論（ヘンキン意味論）を用いて形式化する場合、どのモデルにも集合変数が及ぶ領域が含まれ、この領域は個々の変数の領域の全冪集合の適切な部分集合である可能性がある。^[3]

以下の公理は、基本公理、またはロビンソン公理と呼ばれることもあります。結果として得られる第一階の理論はロビンソン算術と呼ばれ、本質的には帰納法のないペアノ算術です。量化された変数の議論領域は、集合的にNで表され、「ゼロ」と呼ばれる特別なメンバーを含む自然数です。 ${\displaystyle 0}$

基本関数は、接頭辞で表される単項後続関数と、中置演算子"+" と " "で表される2 つの二項演算、加算と乗算です。また、中置演算子 "<" で表される順序と呼ばれる基本二項関係もあります。 ${\displaystyle S}$${\displaystyle \cdot}$

後継関数とゼロを支配する公理:

1. ${\displaystyle \forall m[Sm=0\rightarrow \bot ].}$（「自然数の次の数は決してゼロではない」）
2. ${\displaystyle \forall m\forall n[Sm=Sn\rightarrow m=n].}$（「後続関数は単射である」）
3. ${\displaystyle \forall n[0=n\lor \exists m[Sm=n]].}$（「すべての自然数はゼロかその次の数である」）

再帰的に定義された加算:

4. ${\displaystyle \forall m[m+0=m].}$
5. ${\displaystyle \forall m\forall n[m+Sn=S(m+n)].}$

再帰的に定義された乗算:

6. ${\displaystyle \forall m[m\cdot 0=0].}$
7. ${\displaystyle \forall m\forall n[m\cdot Sn=(m\cdot n)+m].}$

順序関係「<」を支配する公理:

8. ${\displaystyle \forall m[m<0\rightarrow \bot ].}$（「自然数はゼロより小さいことはない」）
9. ${\displaystyle \forall n\forall m[m<Sn\leftrightarrow (m<n\lor m=n)].}$
10. ${\displaystyle \forall n[0=n\lor 0<n].}$（「すべての自然数はゼロかゼロより大きい」）
11. ${\displaystyle \forall m\forall n[(Sm<n\lor Sm=n)\leftrightarrow m<n].}$

これらの公理はすべて一階述語である。つまり、すべての変数は自然数の範囲にあり、その集合の範囲には及ばない。これは、それらが算術的であることよりもさらに強い事実である。さらに、存在量化子は公理 3 に1 つだけある。公理 1 と 2 は、帰納法の公理スキームとともに、Nの通常のペアノ-デデキント定義を構成する。これらの公理に何らかの帰納法の公理スキームを追加すると、公理 3、10、および 11 は不要になる。

φ ( n )が、自由個体変数nと、場合によっては他の自由個体変数または集合変数 ( m ₁ ,..., m _kおよびX ₁ ,..., X _lと表記) を含む 2 階算術の式である場合、φの帰納法公理は次の公理になります。

${\displaystyle \forall m_{1}\dots m_{k}\forall X_{1}\dots X_{l}((\varphi (0)\land \forall n(\varphi (n)\rightarrow \varphi ( Sn)))\rightarrow \forall n\varphi (n))}$

（完全な）2 次帰納法スキームは、すべての 2 次式にわたるこの公理のすべてのインスタンスで構成されます。

帰納的スキームの特に重要な例は、φが式「 」であり、nがXの要素であるという事実を表す場合です（Xは自由集合変数です）。この場合、φの帰納的公理は ${\displaystyle n\in X}$

${\displaystyle \forall X((0\in X\land \forall n(n\in X\rightarrow Sn\in X))\rightarrow \forall n(n\in X))}$

この文は第二階帰納法公理と呼ばれます。

φ ( n ) が自由変数nと他の自由変数を持つ式であるが、変数Z は含まないとすると、φの理解公理は次の式となる。

${\displaystyle \exists Z\forall n(n\in Z\leftrightarrow \varphi (n))}$

この公理により、 φ ( n )を満たす自然数の集合を形成できる。式φには変数Z を含めてはならないという技術的な制約がある。そうでなければ、式は包括公理に繋がってしまうからである。 ${\displaystyle Z=\{n|\varphi (n)\}}$${\displaystyle n\not \in Z}$

${\displaystyle \exists Z\forall n(n\in Z\leftrightarrow n\not \in Z)}$、

これは矛盾しています。この記事の残りの部分ではこの規則を前提としています。

2階算術の形式理論（2階算術の言語で）は、基本公理、あらゆる式φ（算術式またはそれ以外）の理解公理、および2階帰納公理から構成される。この理論は、以下に定義されるサブシステムと区別するために、完全2階算術と呼ばれることもある。完全2階意味論はあらゆる可能な集合が存在することを意味するため、完全2階意味論が採用されている場合、理解公理は演繹システムの一部とみなされる可能性がある。^[3]

このセクションでは、一階意味論を持つ二階算術について説明します。したがって、二階算術の言語モデルは、集合 M (個々の変数の範囲を形成)、定数 0 ( Mの要素)、 MからMへの関数S、 M 上の 2 つの二項演算 + と · 、 M上の二項関係 < 、および集合変数の範囲であるMのサブセットのコレクションDで構成されます。 D を省略すると、一階算術の言語モデルが生成されます。 ${\displaystyle {\mathcal {M}}}$

D がMの完全なべき集合である場合、モデルは完全モデルと呼ばれます。完全な 2 次意味論の使用は、2 次算術のモデルを完全モデルに制限することと同じです。実際、2 次算術の公理には完全なモデルが 1 つしかありません。これは、 2 次帰納法公理を持つペアノ公理には 2 次意味論の下でモデルが 1 つしかないという事実から生じます。 ${\displaystyle {\mathcal {M}}}$

二階算術で証明可能な全関数は、システム Fで表現可能なものとまったく同じです。^{[4]ほぼ同等に、システム F は、ゲーデルの}システム T が弁証法解釈で一階算術に対応するのと並行して、二階算術に対応する関数の理論です。

2 階算術言語のモデルが特定のプロパティを持つ場合、次のような別名で呼ばれることもあります。

• M が通常の自然数集合で通常の演算を伴う場合、 ω-モデルと呼ばれる。この場合、モデルは自然数集合の集合であるDと同一視される。なぜなら、この集合はω-モデルを完全に決定するのに十分だからである。通常の構造とそのすべての部分集合を伴う通常の自然数集合である唯一の完全な -モデルは、意図された、または標準の2次算術モデルと呼ばれる。^[5]${\displaystyle {\mathcal {M}}}$${\displaystyle \omega}$
• 2階算術言語のモデルは、 、すなわち からパラメータを持ちΣ ¹ ₁ステートメントがによって満たされる場合、完全なモデルによって満たされるステートメントと同じである場合、 βモデルと呼ばれます。 ^[6] βモデルに関して絶対的な概念には、「は整列順序をエンコードする」^[7]や「は木である」 ^[6]などがあります。${\displaystyle {\mathcal {M}}}$${\displaystyle {\mathcal {M}}\prec _{1}^{1}{\mathcal {P}}(\omega )}$${\displaystyle {\mathcal {M}}}$${\displaystyle {\mathcal {M}}}$${\displaystyle A\subseteq \omega \times \omega }$${\displaystyle A\subseteq \omega \times \omega }$
• 上記の結果は、のβ _nモデルの概念に拡張されており、 がに置き換えられていることを除いて上記と同じ定義を持ちます。つまり、 はに置き換えられます。 ^[6]この定義を使用すると、 β ₀モデルは ω モデルと同じになります。^[8]${\displaystyle n\in \mathbb {N} }$${\displaystyle \prec _{1}^{1}}$${\displaystyle \prec_{n}^{1}}$${\displaystyle \Sigma _{1}^{1}}$${\displaystyle \Sigma _{n}^{1}}$

2 次演算の名前付きサブシステムは多数あります。

サブシステムの名前の添え字 0 は、完全な 2 次帰納法スキームの制限された部分のみを含むことを示します。^[9]このような制限は、システムの証明理論的強度を大幅に低下させます。たとえば、以下で説明するシステム ACA _0は、ペアノ算術と等価です。対応する理論 ACA は、ACA ₀と完全な 2 次帰納法スキームで構成されており、ペアノ算術よりも強力です。

よく研究されているサブシステムの多くは、モデルの閉包特性に関連しています。たとえば、完全な 2 次演算のすべての ω モデルはチューリング ジャンプの下で閉じていることが示されますが、チューリング ジャンプの下で閉じているすべての ω モデルが完全な 2 次演算のモデルであるとは限りません。サブシステム ACA ₀には、チューリング ジャンプの下での閉包の概念を捉えるのに十分な公理が含まれています。

ACA _{0 は}、基本公理、算術的内包公理体系（言い換えれば、あらゆる算術式φの内包公理）、および通常の 2 階帰納公理からなる理論として定義されます。これは、算術的帰納公理体系全体、つまり、あらゆる算術式φの帰納公理も含めることと同等です。

ωの部分集合Sの集合がACA ₀のωモデルを決定するのは、 Sがチューリングジャンプ、チューリング還元可能性、チューリング結合に関して閉じている場合のみであることが示される。 ^[10]

_{ACA 0}の添え字 0 は、このサブシステムに帰納公理スキームのすべてのインスタンスが含まれているわけではないことを示します。これは、帰納公理のすべてのインスタンスを自動的に満たす ω モデルには影響しません。ただし、非 ω モデルの研究では重要です。ACA ₀とすべての式に対する帰納法で構成されるシステムは、添え字なしの ACA と呼ばれることがあります。

_{ACA 0}システムは、基本公理として定義される一階算術(または一階ペアノ公理)の保守的な拡張であり、一階算術の言語 (クラス変数をまったく許可しない) で一階帰納法公理スキーム (クラス変数をまったく含まないすべての式φに対して) が追加されています。特に、限定された帰納法スキームのため、一階算術と 同じ証明論的順序数ε _{0を持ちます。}

全ての量指定子が ∀ n < tまたは ∃ n < t（ここでnは量化される個々の変数、tは個々の項）の形式である場合、 その式は有界算術式、または Δ ⁰ _{0と呼ばれます。ここで}

${\displaystyle \forall n<t(\cdots )}$

の略

${\displaystyle \forall n(n<t\rightarrow \cdots )}$

そして

${\displaystyle \exists n<t(\cdots )}$

の略

${\displaystyle \exists n(n<t\land \cdots )}$。

式が∃ mの形をしている場合、その式はΣ ⁰ ₁（またはΣ ₁）またはΠ ⁰ ₁（またはΠ ₁ ）と呼ばれる。φ、それぞれ ∀ mφここで、φは有界算術式、m は個体変数（ φにおいて自由）である。より一般的には、存在的個体量指定子、普遍的個体量指定子をそれぞれ Π ⁰ _{n −1 、 Σ 0 n −1}式^に_追加して得られる式は、それぞれ Σ ⁰ _n、 Π ⁰ _nと呼ばれる（そして Σ _{0 0}^とΠ ⁰ _{0は両方とも Δ} ⁰ ₀に等しい）。構造上、これらすべての式は算術的であり（クラス変数は決して有界ではない）、実際、式をスコーレム冠頭形式にすると、十分に大きいnすべてについて、すべての算術式が Σ ⁰ _nまたは Π ⁰ _n式と論理的に同等であることがわかる。

サブシステム RCA _{0は ACA 0}よりも弱いシステムであり、逆数学の基本システムとしてよく使用されます。これは、基本公理、Σ ⁰ ₁帰納法、および Δ ⁰ ₁理解法で構成されます。前者の用語は明確です。Σ ⁰ _{1帰納法は、すべての Σ} ⁰ ₁式φの帰納公理です。「Δ ⁰ ₁理解」という用語はより複雑です。なぜなら、Δ ⁰ ₁式というものは存在しないからです。代わりに、Δ ⁰ _{1理解法は、Π} ⁰ ₁式と論理的に同等であるすべての Σ ⁰ ₁式の理解公理を主張します。このスキームには、すべての Σ ⁰ ₁式φとすべての Π ⁰ ₁式ψについて、次の公理 が含まれます。

${\displaystyle \forall m\forall X((\forall n(\varphi (n)\leftrightarrow \psi (n)))\rightarrow \exists Z\forall n(n\in Z\leftrightarrow \varphi (n)))}$

_{RCA 0}の第一階の結果の集合は、帰納法が Σ ⁰ ₁の式に制限されるペアノ算術のサブシステム IΣ ₁の結果の集合と同じです。同様に、IΣ _{1 は文の}原始再帰算術(PRA)に対して保守的です。さらに、 の証明論的順序数はω ^ωであり、PRA の順序数と同じです。 ${\displaystyle \Pi _{2}^{0}}$${\displaystyle \mathrm {RCA} _{0}}$

ω の部分集合の集合S がRCA ₀の ω モデルを決定するのは、S がチューリング還元可能性とチューリング結合の下で閉じている場合のみであることがわかります。特に、 ω のすべての計算可能な部分集合の集合は、 RCA ₀の ω モデルを与えます。これがこのシステムの名前の由来です。つまり、集合が RCA _{0 を}使用して存在することが証明できる場合、その集合は再帰的 (つまり計算可能) です。

_{時には、RCA 0}よりもさらに弱いシステムが望まれることがあります。そのようなシステムの 1 つは、次のように定義されます。まず、算術言語を指数関数記号で拡張し (より強力なシステムでは、指数は通常のトリックで加算と乗算で定義できますが、システムが弱くなりすぎると、これは不可能になります)、乗算から帰納的に指数を定義する明らかな公理で基本公理を拡張する必要があります。すると、システムは (強化された) 基本公理、Δ ⁰ ₁の理解、および Δ ⁰ ₀の帰納で構成されます。

ACA _{0上では、十分に大きい}nすべてに対して、2 階算術の各式は Σ ¹ _nまたは Π ¹ _n式と同値である。 Π ¹ ₁ -理解体系は、基本公理に加えて、通常の2階帰納公理と、あらゆる (太字^[11] ) Π ¹ ₁式φに対する理解公理からなる体系である。 これは Σ ¹ ₁ -理解と同値である (一方、 Δ ¹ _{1 -理解は Δ} ⁰ _{1 -}理解と同様に定義され、より弱い)。

射影的決定性とは、動きが自然数、ゲームの長さが ω、射影的利得集合であるすべての 2 人用完全情報ゲームが決定されている、つまり、プレーヤーの 1 人が勝利戦略を持っているという主張です。(プレイが利得集合に属する場合、最初のプレーヤーがゲームに勝ちます。そうでない場合は、2 番目のプレーヤーが勝ちます。) 集合が射影的であるためには、(述語として) 2 次算術の言語で式で表現でき、実数をパラメーターとして使用できる必要があります。したがって、射影的決定性は、Z ₂の言語でスキーマとして表現できます。

二次算術の言語で表現できる多くの自然命題は、Z ₂やZFCにさえ依存しないが、射影決定性から証明可能である。例としては、共解析的完全部分集合の性質、可測性、集合に対するベールの性質、均一化などがある。弱基底理論（RCA ₀など）では、射影決定性は理解を意味し、二次算術の本質的に完全な理論を提供する。射影決定性を持つ Z ₂に依存しない Z ₂の言語での自然なステートメントを見つけるのは困難である。^[12]${\displaystyle \Sigma _{2}^{1}}$${\displaystyle \Pi _{3}^{1}}$

ZFC + { n 個 の Woodin 基数があります: nは自然数} は射影決定性を持つZ _{2上で保存的です}^[要出典]。つまり、2 次算術の言語でのステートメントが射影決定性を持つ Z _{2で証明可能であるのは、集合論の言語へのその翻訳が ZFC + {} n個の Woodin 基数があります: n ∈N} で証明可能である場合のみです。

2階算術は自然数と自然数の集合を直接的に形式化します。しかし、コーディング技術を介して間接的に他の数学的対象を形式化することができ、この事実はワイルによって最初に注目されました。[13] 整数、有理数^、実数はすべて、サブシステムRCA _{0で形式化でき、}完全に分離可能な距離空間とそれらの間の連続関数も形式化できます。^[14]

逆数学の研究プログラムでは、数学の定理を証明するために必要な集合存在公理を研究するために、2階算術におけるこれらの数学の形式化を使用しています。^[15]たとえば、実数から実数への関数の中間値定理はRCA ₀で証明可能であり、^[16]ボルツァーノ-ワイエルシュトラスの定理はRCA _{0上のACA 0}と同等です。^[17]

前述のコーディングは、高階基底理論と弱いケーニッヒの補題を仮定すると、連続関数と全関数に対してうまく機能します。^{[18]おそらく予想どおり、}位相 の場合、コーディングに問題がないわけではありません。^[19]

• パリス・ハリントン定理
• プレスブルガー算術
• 真の算術

• バージェス、JP (2005)。『フレーゲの修正』プリンストン大学出版局。
• Buss, SR (1998).証明理論ハンドブック. Elsevier. ISBN 0-444-89840-9。
• 竹内 剛(1975).証明理論. ISBN 0-444-10492-5。