原始帰納的算術

原始帰納的算術（げんしきのうてきさんじゅつ、英: primitive recursive arithmetic）またはPRAは自然数の理論の量化子なしの形式化である。これはトアルフ・スコーレムによって数学基礎論における有限の立場の形式化として提案されたもので、PRAの推論が有限の立場の範疇にあることが広く承認された。また有限の立場がPRAによって捉えきれていると信ぜられているが、有限の立場においても原始再帰よりも強い形の再帰を認めることで（PRAから）拡大することができると信ずる向きもある。それはエプシロン・ノート $\varepsilon _{0}$ までの超限再帰であって、これはペアノ算術の証明論的順序数に等しい。PRAの証明論的順序数は $\omega ^{\omega }$ である。PRAはしばしばスコーレム算術とも呼ばれる。

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

言語と公理

PRAの言語は次のものからなる：

• 可算無限個の変数 x, y, z,....
• 命題結合子
• 等号記号 =, 定数記号 0, 後者記号 S
• 任意の原始帰納的関数に対する記号

PRAの論理公理は次のものからなる：

• 命題論理のトートロジーすべて
• 等号公理

PRAの論理規則はモーダス・ポネンスと変数への代入からなる。非論理公理は次のものからなる：

• $S(x)\neq 0$;
• $S(x)=S(y)~\to ~x=y,$

それと原始帰納的関数の定義式すべてである。例えば原始帰納的関数の最も一般的な特徴付けは、ゼロと後者を含み、射影、関数合成、原始再帰で閉じている、というものである。そこで、(n+1)-変数関数（を表す記号, 以下省略） f が原始再帰によって n-変数の基底関数 g と (n+2)-変数の反復関数 h から得られるときには、次のものを公理とする：

• $f(0,y_{1},\ldots ,y_{n})=g(y_{1},\ldots ,y_{n})$
• $f(S(x),y_{1},\ldots ,y_{n})=h(x,f(x,y_{1},\ldots ,y_{n}),y_{1},\ldots ,y_{n})$

とくに

• $x+0=x\$
• $x+S(y)=S(x+y)\$
• $x\cdot 0=0\$
• $x\cdot S(y)=x\cdot y+x\$
• ... などである。

PRAは一階算術における帰納法公理図式の代わりに次の（量化子なしの）帰納法図式を持つ：

• 任意の述語 $\varphi$ について、 $\varphi (0)$ と $\varphi (x)\to \varphi (S(x))$ から $\varphi (y)$ を導く。

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

論理なしの計算

PRAは形式化において論理記号は不要である - PRAの文は2つの項の間の等号だけであると考えることができる。この設定において項は0またはそれ以上の変数からなる原始帰納的関数である。1941年ハスケル・カリーはそのような体系を与えた。 カリーの体系において帰納法の規則は自然な方法では表現できない。この部分を洗練させたのはグッドスタインである。 グッドスタインの体系において帰納法は次のように表現される：

${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)}.$

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

${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}.$

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

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

${\begin{aligned}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{aligned}}$

すると x=y と |x-y|=0 は同値である。したがって $|x-y|+|u-v|=0\!$ と $|x-y|\cdot |u-v|=0\!$ によって $x=y$ と $u=v$ の論理積と論理和を表すことができる。否定は $1{\dot {-}}|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.