Realizability Interpretation of PA by Iterated Limiting PCA

TL;DR

This paper constructs a hierarchy of partial combinatory algebras (PCAs) through iterated limiting processes, linking realizability interpretations to classical and intuitionistic arithmetic, and analyzing their logical principles.

Contribution

It introduces a hierarchy of PCAs via iterated limiting processes that interpret various logical systems between Heyting's arithmetic and Peano arithmetic.

Findings

The hierarchy captures all arithmetical partial functions.

Kleene's realizability over these PCAs interprets key logical principles.

The work connects realizability, PCA constructions, and logical system interpretations.

Abstract

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, "Limiting partial combinatory algebras" Theoret. Comput. Sci. Vol.311 2004). The n-times iteration of this construction results in a PCA that represents any n-iterated limiting partial recursive functions, 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 \Sigma^0_n-formulas, and that over the latter PCA interprets Peano's arithmetic (PA for short). A hierarchy of logical systems between Heyting's arithmetic and PA is used to discuss the prenex normal form theorem, the relativized independence-of-premise schemes, and "PA is an unbounded extension of HA."