|
原始帰納的算術(げんしきのうてきさんじゅつ、)またはPRAは自然数の理論の量化子なしの形式化である。これはトアルフ・スコーレム〔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.〕によって数学基礎論における有限の立場の形式化として提案されたもので、PRAの推論が有限の立場の範疇にあることが広く承認された。また有限の立場がPRAによって捉えきれていると信ぜられている〔Tait, W.W. (1981), "Finitism", ''Journal of Philosophy'' 78:524-46.〕が、有限の立場においても原始再帰よりも強い形の再帰を認めることで(PRAから)拡大することができると信ずる向きもある。それはエプシロン・ノート までの超限再帰〔Georg Kreisel (1958) "Ordinal Logics and the Characterization of Informal Notions of Proof," ''Proc. Internat. Cong. Mathematicians'': 289-99.〕であって、これはペアノ算術の証明論的順序数に等しい。PRAの証明論的順序数は である。PRAはしばしばスコーレム算術とも呼ばれる。 PRAの言語は自然数と原始帰納的関数からなる算術的命題を表現できる。原始帰納的関数としては例えば加法、乗法、指数関数などが含まれる。PRAは自然数上を走る明示的な量化はできない。PRAはしばしば基本的な証明論(とりわけ一階算術のゲンツェンの無矛盾性証明のような無矛盾性証明)のための超数学的な形式的体系とされる。 == 言語と公理 == PRAの言語は次のものからなる: * 可算無限個の変数 ''x'', ''y'', ''z'',.... * 命題結合子 * 等号記号 ''='', 定数記号 ''0'', 後者記号 ''S'' * 任意の原始帰納的関数に対する記号 PRAの論理公理は次のものからなる: * 命題論理のトートロジーすべて * 等号公理 PRAの論理規則はモーダス・ポネンスと変数への代入からなる。非論理公理は次のものからなる: * ; * それと原始帰納的関数の定義式すべてである。例えば原始帰納的関数の最も一般的な特徴付けは、ゼロと後者を含み、射影、関数合成、原始再帰で閉じている、というものである。そこで、(''n''+1)-変数関数(を表す記号, 以下省略) ''f'' が原始再帰によって ''n''-変数の基底関数 ''g'' と (''n''+2)-変数の反復関数 ''h'' から得られるときには、次のものを公理とする: * * とくに * * * * * ... などである。 PRAは一階算術における帰納法公理図式の代わりに次の(量化子なしの)帰納法図式を持つ: * 任意の述語 について、 と から を導く。 一階算術において、明示的な公理化を必要とする原始帰納的関数は加法と乗法だけである。それ以外の全ての原始帰納的述語はそれら2つの原始帰納的関数と自然数上の量化によって定義できる。(正確にいえば原始帰納的述語を表現する論理式を構成できる。)このような意味の原始帰納的関数の定義はPRAにおいては不可能である。PRAは量化子を欠いているからである。 抄文引用元・出典: フリー百科事典『 ウィキペディア(Wikipedia)』 ■ウィキペディアで「原始帰納的算術」の詳細全文を読む スポンサード リンク
|