About: 原始帰納的算術

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