FANDOM


2階算術 (Second-order arithmetic) (Z2 あるいは \(\Pi_\infty^1\text{-CA}\) としても知られる)は、自然数だけではなく自然数の「集合」の量化を許容する1階述語論理である。

言語 編集

2階算術言語 (language of second-order arithmetic) L2 は、数字そのものと、数字の集合という2種類の対象を議論できる。述語算術を次のように拡張したものである。

  • 無限の数字変数 \(x_0\), \(x_1\), ... と無限の集合変数 \(X_0\), \(X_1\), ...
  • 定数記号ゼロ \(0\)
  • 等号、不等号、集合の要素と呼ばれる3つの二項関係の記号 \(=,<,\in\)。最初の2つは数の間の関係、最後の1つは数と集合の間の関係
  • 数から数へ写す、後者と呼ばれる単項の関数記号 \(S(x)\)
  • 2組の数を1つの数へ移す、それぞれ加法、乗法と呼ばれる2つの二項関数記号 \(+(a,b),\cdot(a,b)\) 。 それらはしばし \(a+b,a\cdot b\) と表示される。

二階算術の言語は自然数とその部分集合だけでなく、整数、有理数、実数、そして実数からなる可算集合(たとえば数列)さえについて語ることができるほど表現に富む。

公理 編集

2階算術理論はペアノの公理に次を加えたものである。

  • 2階帰納公理 \(\forall X (0 \in X \wedge \forall x (x \in X \Rightarrow Sx \in X) \Rightarrow \forall x : x \in X)\) すなわち、ある集合が0を要素に持ち、その集合のすべての要素の後者がその集合の要素である時に、すべての自然数はその集合の要素である。
  • 内包の公理型、 \(X\) が自由変数でないすべての論理式 \(\phi\) ごとに : \(\exists X \forall x (x \in X \Leftrightarrow \phi(x))\) 。すべての自然数に関する述語ごとに自然数の部分集合(すなわち \(\phi\) を満たすこれらの自然数からなる集合)が定義されることを意味する。

サブシステム 編集

Z2 は非常に強力な形式体系であり、多くの場合で、ある結果を証明するためにその強さのすべてを必要とはしない。そのため、Z2 を弱くした時に何が起きるだろうかという疑問が自然にわいてくる。Harvey Friedman は逆数学というプロジェクトを立ち上げた。逆数学とは、ある定理を証明するためにはどの公理が必要であるか、またどの公理系ではその定理を証明するためには不十分か、といった問いに答えるためのものである。

逆数学は二階算術のサブシステムに焦点をおいているが、それは定理の強さを計るために広く研究されてきた。「ビッグファイブ」とはRCA0、WKL0、ACA0、 ATR0、そして \(\Pi_1^1\text{-CA}_0\) である。それぞれのビッグファイブの要素はひとつ前にある要素の真の拡張となっている。専門的な数学に見られる自然数、実数、複素数に関するすべての定理は、ごく一部の例外を除いて、それらを証明するのに必要な最も弱いビッグファイブの要素に基づいて「強さ」を割り当てることができる。それらの多くはRCA0だけで証明されうる。

これらのサブシステムはなお二階算術の「言語」を使っているが、必ずしもその公理を使うわけではない。これらの定理のいくつかは直観的にペアノ算術より弱いかもしれないが、ペアノ算術とは異なり、それらはすべて実数について記述することができる。

RCA0編集

RCA0 の名称の由来は再帰的内包公理 (recursive comprehension axiom)であり、ビッグファイブの中でもっとも弱い。以下で構成される。

  • ロビンソン算術
  • \(\Sigma_1^0\) までの式に制限した first-order schema of induction (算術的階層を参照)
  • \(\Delta_1^0\) までの式に制限した内包公理型

これはいわゆる「基本体系」であり、他のサブシステムはすべて RCA0 の公理を持っている。RCA0 は弱い体系であるが、自然数や実数に関する多くの基本的な性質を証明することができる。たとえば、数列の極限が一意に定まることや、中間値の定理などである。RCA0 は、多くの「日常的に使われる」自然数と実数の性質を証明可能である。

RCA0 は再帰的なものの存在しか証明できる強さを持っていない。たとえば、この理論体系における集合存在公理は、計算不可能な関数の存在を証明する強さを持っていない。

RCA0 の証明論的順序数は \(\omega^\omega\) である。

WKL0編集

WKL0 の名称は弱ケーニヒの補題 (weak König's lemma)に由来する。RCA0 に、次のケーニヒの補題の弱い形式を加えて拡張したものがWKL0 である。

Let \(2^{<\omega}\) be the tree of all finite binary sequences, and let \(T\) be one of its infinite subtrees. Then \(T\) has an infinite branch.

RCA0 はこの補題を証明できない。 無限の計算可能な木 \(T\) で計算可能な無限の枝を持たないものを作ることができるが、RCA0 は計算不可能な集合の存在を証明できないためである。 したがって、 WKL0 は RCA0 の適切な拡張である。

多くの自然な命題が(RCA0の基本理論の元で)WKL0 と同値であることを示すことができる。たとえば、閉区間におけるハイネ・ボレルの被覆定理や、連続関数のリーマン積分可能性などである。もっとも重要な同値な命題の1つは、次の \(\Sigma^0_1\) separation である。Given two \(\Sigma^0_1\) sentences with a free variable \(n\), never both true, there is a set which contains all \(n\) which make first formula true, and none which make second one true.

WKL0 の証明論的順序数は \(\omega^\omega\) であり、RCA0 と同じ consistency strength を持つ。すなわち equiconsistent である。

ACA0編集

算術的内包公理 (Arithmetical comprehension axiom)。 We get this by adjoining to RCA0 axiom schema of comprehension for all arithmetical formulas (ones contained in \(\Sigma_n^0\) for some \(n\in\Bbb N\)). It can be shown that formulas provable in ACA0 which can be expressed in first-order arithmetic are precisely the formulas provable by Peano arithmetic (one says that ACA0 is conservative over Peano arithmetic for arithmetical sentences). Like before, it can be shown that ACA0 is a proper extension of WKL0, although the proof in this case is not as simple.

ACA0 is strong enough to prove all the statements required to work well with real (or complex) analysis, including ボルツァーノ=ワイエルシュトラスの定理 or full König's lemma (for trees on finite sequences of natural numbers) (in fact, ACA0 is provably equivalent to these two statements).

ACA0 has a proof-theoretic ordinal of ε₀.

ATR0編集

This one stands for "arithmetical transfinite recursion". This system is ACA0 together with axiom schema stating, intuitively, that if we have countable well-ordering (coded in a certain way) and so called arithmetical functional, we can iterate application of this functional transfinitely by following the mentioned well-ordering. This means that certain set constructions can be accomplished by iterating a simple construction transfinite number of times.

Addition of this axiom schema makes it possible to build a theory of ordinal numbers in second-order arithmetic. An example of strength of this schema is that it's sufficient to prove the consistency of ACA0, which means that it is significantly stronger than ACA0 (see ゲーデルの不完全性定理).

Important single theorem which is equivalent (over RCA0) to ATR0 is that every two countable well-orderings are comparable, so that ordinal numbers form a linear order.

Another important schema equivalent to ATR0 is \(\Sigma^1_1\) separation: given two \(\Sigma^1_1\) sentences (see 解析的階層) with free variable \(n\), never both true, there is a set which contains all \(n\) which make first formula true, and none which make second one true.

The proof-theoretic ordinal of ATR0 is the フェファーマン・シュッテの順序数.

\(\Pi_1^1\text{-CA}_0\)編集

The last, and the strongest system in the big five is RCA0 extended by \(\Pi_1^1\) comprehension axiom schema, hence the abbreviation. This is so called impredicative system, because it's axioms, in a way, assert existence of objects which depend on the object defined (this is because defining set \(X\) using \(\Pi_1^1\) formula involves statement which is supposed to hold for all sets, including \(X\) itself).

It's clear that \(\Pi_1^1\text{-CA}_0\) contains all the axioms of ACA0, and it can be shown that it also proves all instances of ATR0 axioms, which shows that \(\Pi_1^1\text{-CA}_0\) can build basic theory of ordinal numbers. However, as one can show, statement that given order is well-order is a \(\Pi_1^1\) statement, which means that this last system can show existence of sets definitions of which explicitly use notions of well-ordering, which, in big part, is where the strength of the system comes from.

The proof-theoretic ordinal of \(\Pi_1^1\text{-CA}_0\) is Ψ0ω).

その他のサブシステム 編集

Apart from the Big Five, many subsystems of Z2 have been analysed. Below is the list of more noteworthy ones.

  • RCA, WKL, etc. - these are extensions of corresponding systems RCA0, WKL0, etc. resulting by addition of first-order induction schema for all formulas in language of second-order arithmetic. Indicator of whether this full axiom schema appears in subsystem or not is 0 in the subscript.
  • \(\Sigma_m^n\text{-IND}\), \(\Pi_m^n\text{-IND}\), \(\Delta_m^n\text{-IND}\) - these are schemas of first-order induction limited to \(\Sigma_m^n\), \(\Pi_m^n\), \(\Delta_m^n\) formulas respectively (here and below \(n\) is 0 or 1). Additionally, \(\Pi_\infty^1\text{-IND}\) is conjunction of all of these schemas.
  • \(\Sigma_m^n\text{-TI}\), \(\Pi_m^n\text{-TI}\), \(\Delta_m^n\text{-TI}\) - these are schemas of transfinite induction limited to formulas in respective classes. This means that for every formula \(\psi(n)\) of respective complexity and any well-ordering of natural numbers (coded as some set \(X\)) we can prove \(\forall n:\psi(n)\) by following this well-order. Like above, \(\Pi_\infty^1\text{-TI}\) is conjunction of the above.
  • \(\Sigma_m^n\text{-CA}\), \(\Pi_m^n\text{-CA}\), \(\Delta_m^n\text{-CA}\) - these are schemas of comprehension for respective classes of formulas. Their conjunction, \(\Pi_\infty^1\text{-CA}\), over a weak base system is equivalent to all of Z2.
  • BI - the axiom-schema of bar induction. To state it, we first need a notion of well-founded partial order. We say the ordering \(\prec\) of natural numbers is well-founded if for every set \(X\) the following is true: if for all \(((\forall i\prec j:i\in X)\Rightarrow j\in X)\Rightarrow\forall n:n\in X\). BI states that such an implication is still true if we replace \(n\in X\) by any formula \(\psi(n)\), provided \(a\prec b\) is expressible by arithmetical formula.
  • \(\Sigma_m^n\text{-AC}\), \(\Pi_m^n\text{-AC}\), \(\Delta_m^n\text{-AC}\) - these are schemas "adaptating" ZFC's 選択公理 to second-order arithmetic. They say that if for every \(n\) there is a set \(X\) such that \(\psi(n,X)\) (of complexity asserted by the schema), then we can create sequence of sets \(X_n\) such that \(\psi(n,X_n)\). A variant of this schema is so called weak axiom of choice, which requires that for every \(n\) there is precisely one \(X\) making the formula true.
  • \(\Sigma_m^n\text{-DC}\), \(\Pi_m^n\text{-DC}\), \(\Delta_m^n\text{-DC}\) - these schemas adapt to second-order arithmetic a weak form of the axiom of choice named "axiom of dependent choice". They say that if for every \(n,X\) there is \(Y\) such that \(\psi(n,X,Y)\), then we can find sequence \(X_n\) of sets such that \(\psi(n,X_n,X_{n+1})\). Slight extension to strong dependent choice tells us that the same can be done if we don't assume that such a \(Y\) exists always, but \(\psi(n,X_n,X_{n+1})\) has to hold whenever it exists for \(X_n\).
  • \(\Sigma_m^n\text{-TR}\), \(\Pi_m^n\text{-TR}\), \(\Delta_m^n\text{-TR}\) - these are extensions to arithmetical transfinite recursion to formulas other than arithmetical ones. As before, intuitively, it says that we can iterate certain constructions transfinitely many times.

広告ブロッカーが検出されました。


広告収入で運営されている無料サイトWikiaでは、このたび広告ブロッカーをご利用の方向けの変更が加わりました。

広告ブロッカーが改変されている場合、Wikiaにアクセスしていただくことができなくなっています。カスタム広告ブロッカーを解除してご利用ください。

FANDOMでも見てみる

おまかせWiki