TY - JOUR

T1 - Realizability interpretation of PA by iterated limiting PCA

AU - Akama, Yohji

N1 - Publisher Copyright:
Copyright © 2014 Cambridge University Press.

PY - 2013/10/25

Y1 - 2013/10/25

N2 - 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'.

AB - 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'.

UR - http://www.scopus.com/inward/record.url?scp=84910021283&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84910021283&partnerID=8YFLogxK

U2 - 10.1017/S0960129513000856

DO - 10.1017/S0960129513000856

M3 - Article

AN - SCOPUS:84910021283

VL - 24

JO - Mathematical Structures in Computer Science

JF - Mathematical Structures in Computer Science

SN - 0960-1295

IS - 6

M1 - e240603

ER -