原始帰納的算術
原始帰納的算術（Primitive Recursive Arithmetic, PRA）は、自然数の理論を量化子を用いずに形式化したものです。この体系は、数学基礎論における「有限の立場」を表現する試みとして、トアルフ・スコーレムによって提唱されました。PRAによる推論は有限の立場の範囲内にあると広く認められており、その体系が有限の立場を捉えきれていると考えられています。しかし、有限の立場においても原始帰納よりも強力な再帰を認めることで、PRAを拡張できるとする見解もあります。その拡張は、ε₀までの超限再帰に相当し、ペアノ算術の証明論的順序数と等しくなります。一方、PRA自体の証明論的順序数はω^ωです。PRAは、しばしばスコーレム算術とも呼ばれます。
PRAの言語は、自然数と原始帰納的関数に関する算術的命題を表現できます。原始帰納的関数には、加法、乗法、指数関数などが含まれます。ただし、PRAは自然数に対する明示的な量化を扱うことはできません。PRAは、基本的な証明論、特に一階算術におけるゲンツェンの無矛盾性証明のような、無矛盾性証明のための超数学的な形式体系として用いられます。
PRAの言語は以下の要素で構成されます。
可算無限個の変数: x, y, z, ...
命題結合子
等号記号: =
定数記号: 0
後者記号: S
任意の原始帰納的関数に対する記号
PRAの論理公理は、以下のものからなります。
命題論理のトートロジーすべて
等号公理
PRAの論理規則は、モーダス・ポネンスと変数への代入です。非論理公理は以下の通りです。
S(x) ≠ 0
S(x) = S(y) → x = y
さらに、全ての原始帰納的関数の定義式が含まれます。原始帰納的関数は、ゼロと後者を含み、射影、関数合成、原始再帰で閉じているものとして特徴づけられます。例えば、(n+1)-変数関数 f が、n-変数の基底関数 g と (n+2)-変数の反復関数 h から原始再帰で得られる場合、以下のものが公理となります。
f(0, y₁, ..., yₙ) = g(y₁, ..., yₙ)
f(S(x), y₁, ..., yₙ) = h(x, f(x, y₁, ..., yₙ), y₁, ..., yₙ)
具体例として、加法と乗法の定義式は以下のようになります。
x + 0 = x
x + S(y) = S(x + y)
x ⋅ 0 = 0
x ⋅ S(y) = x ⋅ y + x
PRAは、一階算術における帰納法公理図式の代わりに、以下の量化子なしの帰納法図式を持ちます。
任意の述語φについて、φ(0) と φ(x) → φ(S(x)) から φ(y) を導く。
一階算術では、原始帰納的関数の明示的な公理化が必要なのは加法と乗法のみです。それ以外の全ての原始帰納的述語は、これらの関数と自然数上の量化によって定義できます。しかし、PRAでは量化子が欠けているため、このような原始帰納的述語の定義はできません。
PRAは、論理記号を使わずに形式化できます。PRAの文は、2つの項の間の等号のみであると考えることができます。この場合、項は0または複数の変数を持つ原始帰納的関数です。ハスケル・カリーは1941年にこのような体系を与えました。カリーの体系では、帰納法の規則を自然な形で表現することができませんでしたが、グッドスタインによって洗練されました。グッドスタインの体系では、帰納法は次のように表現されます。
F(0) = G(0) F(S(x)) = H(x, F(x)) G(S(x)) = H(x, G(x))
---------
F(x) = G(x)
ここで、xは変数、Sは後者演算、F, G, Hは原始帰納的関数で、明示されていない他の変数を含んでいても構いません。グッドスタインの体系の残りの規則は以下の代入規則です。
F(x) = G(x)
-----
F(A) = G(A)
A = B
-----
F(A) = F(B)
A = B A = C
--
B = C
ここで、A, B, C は任意の項です。この体系は、論理記号を持たない点を除けば、スコーレムの体系と同様であり、それらに対応する定義式を公理とします。
PRAでは、論理演算を算術的に表現できます。例えば、差の絶対値は以下のように原始帰納的に定義できます。
P(0) = 0
P(S(x)) = x
x -˙ 0 = x
x -˙ S(y) = P(x -˙ y)
|x - y| = (x -˙ y) + (y -˙ x)
この定義により、x = y は |x - y| = 0 と同値になります。したがって、|x - y| + |u - v| = 0 と |x - y| ⋅ |u - v| = 0 は、それぞれ x = y かつ u = v および x = y または u = v を表します。否定は、1 -˙ |x - y| = 0 で表されます。
初等関数算術
ハイティング算術
ペアノ算術
二階算術
原始帰納的関数
Rose, H.E., "On the consistency and undecidability of recursive arithmetic", Zeitschrift für mathematische Logik und Grundlagen der Mathematick Volume 7, pp. 124–135.
Feferman, S (1992) What rests on what? The proof-theoretic analysis of mathematics. Invited lecture, 15th int'l Wittgenstein symposium.
PRAの言語と公理
PRAの言語は、自然数と原始帰納的関数に関する算術的命題を表現できます。原始帰納的関数には、加法、乗法、指数関数などが含まれます。ただし、PRAは自然数に対する明示的な量化を扱うことはできません。PRAは、基本的な証明論、特に一階算術におけるゲンツェンの無矛盾性証明のような、無矛盾性証明のための超数学的な形式体系として用いられます。
PRAの言語は以下の要素で構成されます。
可算無限個の変数: x, y, z, ...
命題結合子
等号記号: =
定数記号: 0
後者記号: S
任意の原始帰納的関数に対する記号
PRAの論理公理は、以下のものからなります。
命題論理のトートロジーすべて
等号公理
PRAの論理規則は、モーダス・ポネンスと変数への代入です。非論理公理は以下の通りです。
S(x) ≠ 0
S(x) = S(y) → x = y
さらに、全ての原始帰納的関数の定義式が含まれます。原始帰納的関数は、ゼロと後者を含み、射影、関数合成、原始再帰で閉じているものとして特徴づけられます。例えば、(n+1)-変数関数 f が、n-変数の基底関数 g と (n+2)-変数の反復関数 h から原始再帰で得られる場合、以下のものが公理となります。
f(0, y₁, ..., yₙ) = g(y₁, ..., yₙ)
f(S(x), y₁, ..., yₙ) = h(x, f(x, y₁, ..., yₙ), y₁, ..., yₙ)
具体例として、加法と乗法の定義式は以下のようになります。
x + 0 = x
x + S(y) = S(x + y)
x ⋅ 0 = 0
x ⋅ S(y) = x ⋅ y + x
帰納法
PRAは、一階算術における帰納法公理図式の代わりに、以下の量化子なしの帰納法図式を持ちます。
任意の述語φについて、φ(0) と φ(x) → φ(S(x)) から φ(y) を導く。
一階算術では、原始帰納的関数の明示的な公理化が必要なのは加法と乗法のみです。それ以外の全ての原始帰納的述語は、これらの関数と自然数上の量化によって定義できます。しかし、PRAでは量化子が欠けているため、このような原始帰納的述語の定義はできません。
論理なしの計算
PRAは、論理記号を使わずに形式化できます。PRAの文は、2つの項の間の等号のみであると考えることができます。この場合、項は0または複数の変数を持つ原始帰納的関数です。ハスケル・カリーは1941年にこのような体系を与えました。カリーの体系では、帰納法の規則を自然な形で表現することができませんでしたが、グッドスタインによって洗練されました。グッドスタインの体系では、帰納法は次のように表現されます。
F(0) = G(0) F(S(x)) = H(x, F(x)) G(S(x)) = H(x, G(x))
---------
F(x) = G(x)
ここで、xは変数、Sは後者演算、F, G, Hは原始帰納的関数で、明示されていない他の変数を含んでいても構いません。グッドスタインの体系の残りの規則は以下の代入規則です。
F(x) = G(x)
-----
F(A) = G(A)
A = B
-----
F(A) = F(B)
A = B A = C
--
B = C
ここで、A, B, C は任意の項です。この体系は、論理記号を持たない点を除けば、スコーレムの体系と同様であり、それらに対応する定義式を公理とします。
論理演算の算術的表現
PRAでは、論理演算を算術的に表現できます。例えば、差の絶対値は以下のように原始帰納的に定義できます。
P(0) = 0
P(S(x)) = x
x -˙ 0 = x
x -˙ S(y) = P(x -˙ y)
|x - y| = (x -˙ y) + (y -˙ x)
この定義により、x = y は |x - y| = 0 と同値になります。したがって、|x - y| + |u - v| = 0 と |x - y| ⋅ |u - v| = 0 は、それぞれ x = y かつ u = v および x = y または u = v を表します。否定は、1 -˙ |x - y| = 0 で表されます。
関連項目
初等関数算術
ハイティング算術
ペアノ算術
二階算術
原始帰納的関数
参考文献
Rose, H.E., "On the consistency and undecidability of recursive arithmetic", Zeitschrift für mathematische Logik und Grundlagen der Mathematick Volume 7, pp. 124–135.
外部リンク
Feferman, S (1992) What rests on what? The proof-theoretic analysis of mathematics. Invited lecture, 15th int'l Wittgenstein symposium.
もう一度検索
【記事の利用について】
タイトルと記事文章は、記事のあるページにリンクを張っていただければ、無料で利用できます。
※画像は、利用できませんのでご注意ください。
【リンクついて】
リンクフリーです。