Realizability interpretation of PA by iterated limiting PCA

研究成果: Article査読

1 被引用数 (Scopus)


For any partial combinatory algebra (PCA for short) A, the class of A-representable partial functions from N to A quotiented by the filter of cofinite sets of N is a PCA such that the representable partial functions are exactly the limiting partial functions of A-representable partial functions (Akama 2004). The n-times iteration of this construction results in a PCA that represents any n-iterated limiting partial recursive function, and the inductive limit of the PCAs over all n is a PCA that represents any arithmetical partial function. Kleene's realizability interpretation over the former PCA interprets the logical principles of double negation elimination for Σ0 n-formulae, and over the latter PCA, it interprets Peano's arithmetic (PA for short). A hierarchy of logical systems between Heyting's arithmetic (HA for short) and PA is used to discuss the prenex normal form theorem, relativised independence-of-premise schemes, and the statement 'PA is an unbounded extension of HA'.

ジャーナルMathematical Structures in Computer Science
出版ステータスPublished - 2013 10 25

ASJC Scopus subject areas

  • 数学(その他)
  • コンピュータ サイエンスの応用


「Realizability interpretation of PA by iterated limiting PCA」の研究トピックを掘り下げます。これらがまとまってユニークなフィンガープリントを構成します。