原始帰納的算術

ウィキペディア

原始帰納的算術

出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2022/08/01 07:48 UTC 版)

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