Realizability interpretation of PA by iterated limiting PCA

Research output: Contribution to journalArticlepeer-review

1 Citation (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'.

Original languageEnglish
Article numbere240603
JournalMathematical Structures in Computer Science
Issue number6
Publication statusPublished - 2013 Oct 25


Dive into the research topics of 'Realizability interpretation of PA by iterated limiting PCA'. Together they form a unique fingerprint.

Cite this