二階算術

提供: testwiki
ナビゲーションに移動 検索に移動

数理論理学における二階算術（にかいさんじゅつ、テンプレート:Lang-en-short）は、自然数およびその部分集合を形式化する公理系の総称である。数学の基礎としては公理的集合論と並ぶ選択肢であり、すべてではないが多くの数学を展開できる。

三階の変数を許す二階算術の先駆的な体系は、ダフィット・ヒルベルトとパウル・ベルナイスの共著書 テンプレート:仮リンク で導入された[1]。二階算術の標準的な公理化は Z2 で表される。

二階算術は一階の対応物であるペアノ算術を含むが、それより本質的に強い。ペアノ算術と違い、二階算術は数そのものだけでなく自然数の集合に対する量化も許す。実数は自然数の（無限）集合として周知の方法で表現できるため、二階算術は実数を形式化できる。この理由から、二階算術は「解析」とも呼ばれる[2]。

また、二階算術は「あらゆる要素が自然数か自然数の集合である」ような集合論の弱いバージョンとも見なせる。ツェルメロ＝フレンケル集合論よりずっと弱いにもかかわらず、二階算術はその言語で表現できる古典数学の結果のほとんどを証明できる。

二階算術の部分体系とは、その各公理が完全な二階算術（Z2）の定理であるような、二階算術の言語における理論である。このような部分体系は、逆数学——古典数学のどれだけが、さまざまな強さの弱い部分体系においてどの程度導出できるかを調べる研究計画——にとって本質的である。核となる数学の多くはこれら弱い部分体系（その一部は下に定義される）で形式化でき、逆数学はさらに古典数学がどの程度・どのような仕方で非構成的であるかを明らかにする。

定義

構文

二階算術の言語は テンプレート:仮リンクである。第一のソートのテンプレート:仮リンクおよび変数は通常小文字で表され、自然数として解釈される個体を表す。もう一方の「集合変数」「クラス変数」あるいは「述語」と呼ばれる変数は通常大文字で表される。これらは個体のクラス／述語／性質を指し、したがって自然数の集合と考えられる。個体変数・集合変数の両方は全称的にも存在的にも量化できる。集合変数の束縛がまったくない（すなわち集合変数を量化する量化子を含まない）式は算術的と呼ばれる。算術的な式は自由な集合変数と束縛された個体変数を持ちうる。

個体項は定数 0、単項関数 S（後者関数）、二項演算 + と ⋅（加法と乗法）から構成される。後者関数は入力に 1 を加える。関係 =（等号）と <（自然数の大小比較）は2つの個体を関係づけ、関係 ∈（帰属）は個体と集合（またはクラス）を関係づける。すなわち、二階算術の言語のシグネチャは ℒ={0,S,+,⋅,=,<,∈} で与えられる。

例えば ∀n(n∈X→Sn∈X) は算術的な二階算術の整式で、1つの自由集合変数 X と1つの束縛個体変数 n を持つ（算術的な式に要求される通り、束縛集合変数はない）。一方、∃X∀n(n∈X↔n<SSSSSS0⋅SSSSSSS0) は整式であるが算術的ではなく、束縛集合変数 X と束縛個体変数 n を持つ。

意味論

量化子にはいくつかの異なる解釈が可能である。もし二階論理の完全な意味論のもとで二階算術を研究するなら、集合量化子は個体変数の範囲のすべての部分集合を渡る。もし二階算術を一階論理の意味論（ヘンキン意味論）で形式化するなら、任意のモデルは集合変数が渡る領域を含み、その領域は個体変数の領域の完全な冪集合の真部分集合であってもよい[3]。

公理

基本公理

以下の公理は基本公理、あるいはロビンソン公理として知られる。それから得られる一階理論はロビンソン算術として知られ、本質的に帰納法なしのペアノ算術である。量化変数の議論領域は自然数全体（総称して N と書き、区別された元 0「ゼロ」を含む）である。

原始関数は接頭辞 S で表される単項の後者関数と、中置演算子 "+" および "⋅" で表される二項演算 加法・乗法である。また、中置演算子 "<" で表される順序と呼ばれる原始的な二項関係も存在する。

後者関数と 0 に関する公理:

  1. ∀m[Sm=0→⊥].（「自然数の後者は決して 0 ではない」）
  2. ∀m∀n[Sm=Sn→m=n].（「後者関数は単射である」）
  3. ∀n[0=n∨∃m[Sm=n]].（「すべての自然数は 0 または後者である」）

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

  2. ∀m[m+0=m].
  3. ∀m∀n[m+Sn=S(m+n)].

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

  2. ∀m[m⋅0=0].
  3. ∀m∀n[m⋅Sn=(m⋅n)+m].

順序関係 "<" に関する公理:

  2. ∀m[m<0→⊥].（「0 より小さい自然数は存在しない」）
  3. ∀n∀m[m<Sn↔(m<n∨m=n)].
  4. ∀n[0=n∨0<n].（「すべての自然数は 0 または 0 より大きい」）
  5. ∀m∀n[(Sm<n∨Sm=n)↔m<n].

これらの公理はすべて一階の言明である。すなわち、すべての変数は自然数を範囲とし、その集合は範囲としない。これは算術的であることよりもさらに強い事実である。加えて、存在量化子は公理 3 の中に1つあるのみである。公理 1 と 2、および帰納法公理図式を合わせると、通常のNのペアノ＝デデキント定義になる。これらの公理に何らかの帰納法公理図式を加えると、公理 3・10・11 は冗長となる。

帰納法と分出図式

φ(n) を二階算術の式で、自由な個体変数 n と、場合によっては他の自由な個体変数または集合変数（m1,...,mk と X1,...,Xl）を含むものとする。φ に対する帰納法公理は

∀m1…mk∀X1…Xl((φ(0)∧∀n(φ(n)→φ(Sn)))→∀nφ(n))

（完全な）二階帰納法図式は、この公理のすべての二階式にわたるインスタンスから成る。

帰納法図式の特に重要なインスタンスは、φ が「n∈X」という、n が X の元であるという事実を表す式のときである（X は自由集合変数）。この場合、φ に対する帰納法公理は

∀X((0∈X∧∀n(n∈X→Sn∈X))→∀n(n∈X))

となる。この文は二階帰納法公理と呼ばれる。

φ(n) が自由変数 n（および場合によっては他の自由変数、ただし変数 Z は含まない）を持つ式ならば、φ に対する内包公理は

∃Z∀n(n∈Z↔φ(n))

である。

この公理により、φ(n) を満たす自然数の集合 Z={n|φ(n)} を形成できる。式 φ が変数 Z を含まないという技術的制限があるのは、そうでなければ式 n∉Z が矛盾する分出公理

∃Z∀n(n∈Z↔n∉Z)

を導くからである。以下、この規約を仮定する。

完全な体系

（二階算術の言語における）二階算術の形式理論は、基本公理・すべての式 φ に対する分出公理・二階帰納法公理からなる。この理論は、後述の部分体系と区別するため完全な二階算術と呼ばれることがある。完全な二階意味論はすべての可能な集合が存在することを含意するため、完全な二階意味論を採用する場合、分出公理は演繹系の一部と見なすこともできる[3]。

モデル

この節では一階意味論を伴う二階算術を記述する。二階算術の言語のモデル ℳ は集合 M（個体変数の範囲を成す）と、定数 0（M の元）、M から M への関数 S、M 上の二項演算 + と ·、M 上の二項関係 <、そして集合変数の範囲となる M の部分集合の族 D から成る。D を除くと一階算術の言語のモデルが得られる。

D が M の完全な冪集合であるとき、モデル ℳ は完全モデルと呼ばれる。完全な二階意味論の使用は、二階算術のモデルを完全モデルに制限することと等価である。実際、二階算術の公理は唯一の完全モデルしか持たない。これは、ペアノの公理が二階帰納法公理付きで二階意味論のもとで唯一のモデルしか持たないという事実から従う。

定義可能な関数

二階算術の中で証明可能にテンプレート:仮リンクである一階関数は、システム F で表現可能なものと完全に一致する[4]。ほとんど同等に、システム F はテンプレート:仮リンクにおいて一階算術がゲーデルのテンプレート:仮リンクに対応するのと並行して、二階算術に対応する汎関数の理論である。

モデルの種類

二階算術の言語のモデルが特定の性質を持つとき、以下のような別の名前でも呼ばれる:

  • M が通常の演算を備えた通常の自然数の集合であるとき、ℳ はω-モデルと呼ばれる。この場合、集合 D（自然数の集合の族）だけで ω-モデル を完全に決定できるので、モデルは D と同一視できる。通常の構造とすべての部分集合を持つ通常の自然数の集合という唯一の完全な ω-モデルは、二階算術の意図されたあるいは標準モデルと呼ばれる[5]。
  • 二階算術の言語のモデル ℳ は、ℳ≺11𝒫(ω)——すなわち ℳ からのパラメータを持つ、ℳ で満たされるΣ11-言明が完全モデルで満たされるものと同じ——のとき、β-モデルと呼ばれる[6]。β-モデルに関して絶対な概念には「A⊆ω×ω が整列順序をコードする」[7]、「A⊆ω×ω がテンプレート:仮リンクである」[6]などがある。
  • 上記の結果は n∈ℕ に対するβn-モデルの概念に拡張されており、これは上記の定義で ≺11 を ≺n1 に、すなわち Σ11 を Σn1 に置き換えたものである[6]。この定義のもとで β0-モデル は ω-モデル と同じとなる[8]。

部分体系

テンプレート:Main

二階算術には多くの名前付き部分体系がある。

部分体系名の添字 0 は、その体系が完全な二階帰納法図式の一部分だけを含むことを示す[9]。この制限は体系のテンプレート:仮リンクを大幅に下げる。例えば、下に説明する体系 ACA0 はペアノ算術とテンプレート:仮リンクである。対応する理論 ACA（ACA0 に完全な二階帰納法図式を加えたもの）はペアノ算術より強い。

算術的分出

よく研究された部分体系の多くはモデルの閉包性質と関連する。例えば、完全な二階算術のすべての ω-モデルはチューリングジャンプについて閉じているが、チューリングジャンプについて閉じたすべての ω-モデルが完全な二階算術のモデルとは限らない。部分体系 ACA0 は、チューリングジャンプ閉包の概念を捉えるちょうど十分な公理を含む。

ACA0 は、基本公理・算術的分出公理図式（すなわちすべての算術的な式 φ に対する分出公理）・通常の二階帰納法公理からなる理論と定義される。算術的帰納法公理図式全体（すなわちすべての算術的式 φ に対する帰納法公理）を含めても等価である。

ω の部分集合の族 S が ACA0 の ω-モデルを決定するのは、S がチューリングジャンプ・チューリング還元・チューリング結合について閉じているとき、かつそのときに限るテンプレート:Sfn。

ACA0 の添字 0 は、この部分体系に帰納法公理図式のすべてのインスタンスが含まれるわけではないことを示す。これは自動的に帰納法公理のすべてのインスタンスを満たす ω-モデルには関係ないが、非 ω-モデルの研究では重要である。ACA0 にすべての式に対する帰納法を加えた体系は、添字なしの ACA と呼ばれることがある。

体系 ACA0 は、一階算術（あるいは一階ペアノ公理、すなわち基本公理と、一階算術の言語における一階帰納法公理図式（束縛されるされないにかかわらずクラス変数を全く含まないすべての式 φ に対する）からなる）の保存拡大である。特に、限定された帰納法図式のため、一階算術と同じテンプレート:仮リンク ε0 を持つ。

式の算術的階層

テンプレート:Main

式は、そのすべての量化子が ∀n<t か ∃n<t（n は量化される個体変数、t は個体項）の形であるとき、有界算術的または Δ00 と呼ばれる。ここで

∀n<t(⋯)

は

∀n(n<t→⋯)

を表し、

∃n<t(⋯)

は

∃n(n<t∧⋯)

を表す。

式は、有界算術式 φ と個体変数 m（φ の中で自由）に対して ∃mφ の形であるとき Σ01（あるいは Σ1）と呼ばれ、∀mφ の形であるとき Π01（あるいは Π1）と呼ばれる。より一般に、式は Π0n−1 あるいは Σ0n−1 の式に存在／全称の個体量化子を加えることで得られるとき、それぞれ Σ0n あるいは Π0n と呼ばれる（Σ00 と Π00 はどちらも Δ00 と等しい）。構成により、これらの式はすべて算術的（クラス変数は決して束縛されない）である。実際、式をスコーレム冠頭形式に置くことで、任意の算術的式は十分大きな n についてある Σ0n または Π0n の式と論理的に等価であることがわかる。

再帰的分出

部分体系 RCA0 は ACA0 より弱い体系で、逆数学の基礎体系としてしばしば用いられる。これは基本公理、Σ01 帰納法図式、Δ01 分出図式からなる。前者は明確である。すなわち Σ01 帰納法図式はすべての Σ01 式 φ に対する帰納法公理である。「Δ01 分出」の用語はより複雑で、というのも Δ01 式というものは存在しないからである。Δ01 分出図式は代わりに、Π01 式と論理的に等価な Σ01 式に対する分出公理を主張する。この図式は各 Σ01 式 φ と各 Π01 式 ψ に対して以下の公理を含む:

∀m∀X((∀n(φ(n)↔ψ(n)))→∃Z∀n(n∈Z↔φ(n)))

RCA0 の一階論理的帰結の集合は、帰納法が Σ01 式に制限されたペアノ算術の部分体系 IΣ1 のそれと同じである。さらに IΣ1 は Π20 文について原始帰納的算術 (PRA) 上の保存拡大である。加えて、RCA0 の証明論的順序数は PRA と同じ ωω である。

ω の部分集合の族 S が RCA0 の ω-モデルを決定するのは、S がチューリング還元とチューリング結合について閉じているとき、かつそのときに限ることがわかる。特に、ω の全計算可能な部分集合の族は RCA0 の ω-モデルを与える。これがこの体系の名前の動機である——ある集合が RCA0 を使って存在を証明できれば、その集合は再帰的（すなわち計算可能）である。

より弱い体系

RCA0 よりさらに弱い体系が必要な場合もある。そのような体系の一つは以下のように定義される: まず算術の言語に指数関数記号を追加し（より強い体系では通常のトリックで指数を加法と乗法を用いて定義できるが、体系が弱くなり過ぎるとこれはできなくなる）、基本公理に、乗法から帰納的に指数関数を定義する明白な公理を追加する。次に体系は（拡張された）基本公理と Δ01 分出および Δ00 帰納法からなる。

より強い体系

ACA0 上では、二階算術の各式は十分大きな n についてある Σ1n または Π1n の式と等価である。体系 Π11-分出 は基本公理・通常の二階帰納法公理・すべての（テンプレート:仮リンク[10]）Π11 式 φ に対する分出公理からなる体系である。これは Σ11-分出と等価である（一方、Δ01-分出と類比的に定義された Δ11-分出はより弱い）。

射影決定性

テンプレート:Main テンプレート:仮リンクは、自然数を手番とし長さ ω で射影的な報酬集合を持つ2人完全情報ゲームがすべて決定的である——すなわちいずれかのプレイヤーが必勝戦略を持つ——という主張である（プレイが報酬集合に属するとき最初のプレイヤーが勝ち、そうでないとき2番目のプレイヤーが勝つ）。集合が射影的であるのは、（述語として）実数をパラメータとして許した二階算術の言語における式で表現可能なとき、かつそのときに限る。したがって射影決定性は Z2 の言語における図式として表現できる。

二階算術の言語で表現できる自然な命題の多くは Z2 やZFC にすら独立だが、射影決定性から証明可能である。例として、余解析的な完全集合性質、Σ21 集合の可測性とベールの性質、Π31 テンプレート:仮リンクなどがある。弱い基礎理論（RCA0 のような）上では、射影決定性は分出を含意し、二階算術の本質的に完全な理論を提供する——射影決定性付きの Z2 と独立な、Z2 の言語における自然な言明を見つけるのは難しい[11]。

ZFC + {n 個のテンプレート:仮リンクが存在する: n は自然数} は射影決定性付きの Z2 上で保存的であるテンプレート:要出典。すなわち、二階算術の言語における言明は、それが射影決定性付きの Z2 で証明可能なのは、その集合論の言語への翻訳が ZFC + {n 個のウッディン基数が存在する: n∈N} で証明可能なとき、かつそのときに限る。

数学のコード化

二階算術は自然数と自然数の集合を直接的に形式化する。しかし、コード化技法によって他の数学的対象を間接的に形式化することもでき、これはワイルによって最初に指摘されたテンプレート:Sfn。整数・有理数・実数はすべて部分体系 RCA0 で形式化できる。同様に完備可分距離空間およびその間の連続関数も形式化できる[12]。

逆数学の研究計画は、これらの二階算術における数学の形式化を利用して、数学の定理を証明するために必要な集合の存在公理を研究するテンプレート:Sfn。例えば、実数から実数への関数に対する中間値の定理は RCA0 で証明可能であるテンプレート:Sfnが、ボルツァーノ＝ワイエルシュトラスの定理は RCA0 上で ACA0 と等価であるテンプレート:Sfn。

上記のコード化は連続で全域な関数についてはうまくいく（高階基礎理論プラス弱ケーニヒの補題を仮定して）[13]。予想通り、位相論の場合コード化には問題がないわけではない[14]。

関連項目

脚注

テンプレート:脚注ヘルプ テンプレート:Reflist

  1. ↑ 引用エラー: 無効な <ref> タグです。「hilbert-bernays」という名前の注釈に対するテキストが指定されていません
  2. ↑ 引用エラー: 無効な <ref> タグです。「sieg」という名前の注釈に対するテキストが指定されていません
  3. ↑ 3.0 3.1 引用エラー: 無効な <ref> タグです。「shapiro」という名前の注釈に対するテキストが指定されていません
  4. ↑ 引用エラー: 無効な <ref> タグです。「girard」という名前の注釈に対するテキストが指定されていません
  5. ↑ 引用エラー: 無効な <ref> タグです。「simpson」という名前の注釈に対するテキストが指定されていません
  6. ↑ 6.0 6.1 6.2 引用エラー: 無効な <ref> タグです。「marek-stable」という名前の注釈に対するテキストが指定されていません
  7. ↑ 引用エラー: 無効な <ref> タグです。「marek-models」という名前の注釈に対するテキストが指定されていません
  8. ↑ 引用エラー: 無効な <ref> タグです。「marek-observations」という名前の注釈に対するテキストが指定されていません
  9. ↑ 引用エラー: 無効な <ref> タグです。「friedman」という名前の注釈に対するテキストが指定されていません
  10. ↑ 引用エラー: 無効な <ref> タグです。「welch」という名前の注釈に対するテキストが指定されていません
  11. ↑ 引用エラー: 無効な <ref> タグです。「woodin」という名前の注釈に対するテキストが指定されていません
  12. ↑ テンプレート:Harvnb, 第 II 章。
  13. ↑ 引用エラー: 無効な <ref> タグです。「kohlenbach」という名前の注釈に対するテキストが指定されていません
  14. ↑ 引用エラー: 無効な <ref> タグです。「hunter」という名前の注釈に対するテキストが指定されていません
「https://ja.wiki.beta.math.wmflabs.org/w/index.php?title=二階算術&oldid=14353」から取得