原始帰納的算術

出典: フリー百科事典『ウィキペディア(Wikipedia)』

移動: 案内検索

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

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

言語と公理[編集]

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

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

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

  • S(x) \ne 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年ハスケル・カリーはそのような体系を与えた。[4] カリーの体系において帰納法の規則は自然な方法では表現できない。この部分を洗練させたのはグッドスタインである。[5] グッドスタインの体系において帰納法は次のように表現される:

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

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

関連項目[編集]

参考文献[編集]

  1. ^ 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.
  2. ^ Tait, W.W. (1981), "Finitism", Journal of Philosophy 78:524-46.
  3. ^ Georg Kreisel (1958) "Ordinal Logics and the Characterization of Informal Notions of Proof," Proc. Internat. Cong. Mathematicians: 289-99.
  4. ^ Haskell Curry, A Formalization of Recursive Arithmetic. American Journal of Mathematics, vol 63 no 2 (1941) pp 263-282
  5. ^ Reuben Goodstein, Logic-free formalisations of recursive arithmetic, Mathematica Scandinavica vol 2 (1954) pp 247-261
  • 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.