原始帰納的算術のソースを表示

'''原始帰納的算術'''（げんしきのうてきさんじゅつ、{{lang-en-short|primitive recursive arithmetic}}）または'''PRA'''は[[自然数]]の理論の[[量化子]]なしの形式化である。これは[[トアルフ・スコーレム]]<ref>[[Thoralf Skolem]] (1923) "The foundations of elementary arithmetic" in [[Jean van Heijenoort]], translator and ed. (1967) ''From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931''. Harvard Univ. Press: 302-33.</ref>によって[[数学基礎論]]における[[有限の立場]]の形式化として提案されたもので、PRAの推論が有限の立場の範疇にあることが広く承認された。また有限の立場がPRAによって捉えきれていると信ぜられている<ref>[[William W. Tait|Tait, W.W.]] (1981), "Finitism", ''Journal of Philosophy'' 78:524-46.</ref>が、有限の立場においても原始再帰よりも強い形の再帰を認めることで（PRAから）拡大することができると信ずる向きもある。それは[[エプシロン・ノート]] <math>\varepsilon_0</math> までの超限再帰<ref>[[Georg Kreisel]] (1958) "Ordinal Logics and the Characterization of Informal Notions of Proof," ''Proc. Internat. Cong. Mathematicians'': 289-99.</ref>であって、これは[[ペアノ算術]]の[[証明論的順序数]]に等しい。PRAの証明論的順序数は <math>\omega^\omega</math> である。PRAはしばしば'''スコーレム算術'''とも呼ばれる。

PRAの言語は[[自然数]]と[[原始帰納的関数]]からなる算術的命題を表現できる。原始帰納的関数としては例えば[[加法]]、[[乗法]]、[[指数関数]]などが含まれる。PRAは自然数上を走る明示的な量化はできない。PRAはしばしば基本的な[[証明論]]（とりわけ[[一階算術]]の{{仮リンク|ゲンツェンの無矛盾性証明|en|Gentzen's consistency proof|preserve=1}}のような[[無矛盾性証明]]）のための[[超数学]]的な[[形式的体系]]とされる。

== 言語と公理 ==
PRAの言語は次のものからなる：
* [[可算無限]]個の変数 ''x'', ''y'', ''z'',....
* [[命題論理|命題]]結合子
* 等号記号 ''='', 定数記号 ''0'', [[原始帰納的関数|後者]]記号 ''S''
* 任意の[[原始帰納的関数]]に対する記号

PRAの論理公理は次のものからなる：
* [[命題論理]]の[[トートロジー]]すべて
* [[等号公理]]
PRAの論理規則は[[モーダス・ポネンス]]と[[一階述語論理#代入について|変数への代入]]からなる。非論理公理は次のものからなる：
* <math>S(x) \ne 0</math>;
* <math>S(x)=S(y) ~\to~ x=y,</math>
それと[[原始帰納的関数]]の定義式すべてである。例えば原始帰納的関数の最も一般的な特徴付けは、ゼロと後者を含み、射影、関数合成、原始再帰で閉じている、というものである。そこで、(''n''+1)-変数関数（を表す記号, 以下省略） ''f'' が原始再帰によって ''n''-変数の基底関数 ''g'' と (''n''+2)-変数の反復関数 ''h'' から得られるときには、次のものを公理とする：
* <math>f(0,y_1,\ldots,y_n) = g(y_1,\ldots,y_n)</math>
* <math>f(S(x),y_1,\ldots,y_n) = h(x,f(x,y_1,\ldots,y_n),y_1,\ldots,y_n)</math>
とくに
* <math>x+0 = x\ </math>
* <math>x+S(y) = S(x+y)\ </math>
* <math>x \cdot 0 = 0\ </math>
* <math>x \cdot S(y) = x \cdot y + x\ </math>
* ... などである。
PRAは[[一階算術]]における[[数学的帰納法|帰納法]][[公理図式]]の代わりに次の（量化子なしの）帰納法図式を持つ：
* 任意の述語 <math>\varphi</math> について、 <math>\varphi(0)</math> と <math>\varphi(x)\to\varphi(S(x))</math> から <math>\varphi(y)</math> を導く。

[[一階算術]]において、明示的な公理化を必要とする[[原始帰納的関数]]は[[加法]]と[[乗法]]だけである。それ以外の全ての原始帰納的述語はそれら2つの原始帰納的関数と[[自然数]]上の[[量化子|量化]]によって定義できる。（正確にいえば原始帰納的述語を表現する論理式を構成できる。）このような意味の原始帰納的関数の定義はPRAにおいては不可能である。PRAは量化子を欠いているからである。

== 論理なしの計算 ==
PRAは形式化において論理記号は不要である - PRAの文は2つの項の間の等号だけであると考えることができる。この設定において項は0またはそれ以上の変数からなる原始帰納的関数である。1941年[[ハスケル・カリー]]はそのような体系を与えた。<ref>[[Haskell Curry]], ''[http://www.jstor.org/stable/2371522 A Formalization of Recursive Arithmetic]''. [[American Journal of Mathematics]], vol 63 no 2 (1941) pp 263-282</ref> カリーの体系において帰納法の規則は自然な方法では表現できない。この部分を洗練させたのは[[グッドスタイン]]である。<ref>[[Reuben Goodstein]], ''[http://www.digizeitschriften.de/resolveppn/GDZPPN002343355 Logic-free formalisations of recursive arithmetic]'', [[Mathematica Scandinavica]] vol 2 (1954) pp 247-261</ref> グッドスタインの体系において帰納法は次のように表現される：

<math>{F(0) = G(0) \quad F(S(x)) = H(x,F(x)) \quad G(S(x)) = H(x,G(x)) \over F(x) = G(x)}.</math>

ここで ''x'' は変数、''S'' は後者演算、''F'', ''G'', ''H'' は原始帰納的関数であり、ここに明示した以外の変数を含んでいてもよい。グッドスタインの体系の残る規則は次の代入規則である：

<math>{F(x) = G(x) \over F(A) = G(A)} \qquad {A = B \over F(A) = F(B)} \qquad {A = B \quad A = C \over B = C}.</math>

ここで ''A'', ''B'', ''C'' は任意の項（0またはそれ以上の変数からなる原始帰納的関数）である。言語は論理記号を持たない点を除けば、上に述べたスコーレムの体系と同様であり、またそれらに対応する定義式を公理とする。命題論理のトートロジーや論理規則は持たない。

論理演算は算術的に表現することができる。例えば、差の絶対値は次のように原始再帰的に定義できる：

<math>
\begin{align} 
P(0) = 0 \quad & \quad P(S(x)) = x \\ 
x \dot - 0 = x \quad & \quad x \dot - S(y) = P(x \dot - y) \\
|x - y| = & (x \dot - y) + (y \dot - x). \\
\end{align}
</math>

すると x=y と |''x''-''y''|=0 は同値である。したがって <math>|x - y| + |u - v| = 0 \!</math> と <math>|x - y| \cdot |u - v| = 0 \!</math> によって <math>x=y</math> と <math>u=v</math> の[[論理積]]と[[論理和]]を表すことができる。[[否定]]は <math>1 \dot - |x - y| = 0</math> と表せる。

== 関連項目 ==
* [[初等関数算術]]
* [[ハイティング算術]]
* [[ペアノ算術]]
* [[二階算術]]
* [[原始帰納的関数]]

==参考文献==
<references/>
* Rose, H.E., "On the consistency and undecidability of recursive arithmetic", ''Zeitschrift für mathematische Logik und Grundlagen der Mathematick'' Volume 7, pp.&nbsp;124–135.

==外部リンク==
* [[Solomon Feferman|Feferman, S]] (1992) ''[http://citeseer.ist.psu.edu/feferman92what.html What rests on what? The proof-theoretic analysis of mathematics]''. Invited lecture, 15th int'l Wittgenstein symposium.

{{デフォルトソート:けんしきのうてきさんしゆつ}}
[[Category:算術の形式理論]]
[[Category:構成主義 (数学)]]
[[Category:数学に関する記事]]