Realizability interpretation of PA by iterated limiting PCA

DOI10.1017/S0960129513000856zbMATH Open1342.03039arXiv1307.5521MaRDI QIDQ5740403FDOQ5740403

Authors: Yohji Akama 

Publication date: 26 July 2016

Published in: Mathematical Structures in Computer Science (Search for Journal in Brave)

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."

Full work available at URL: https://arxiv.org/abs/1307.5521

Recommendations

• Minimal readability of intuitionistic arithmetic and elementary analysis
• scientific article; zbMATH DE number 1841833
• Theory and Applications of Models of Computation
• Effective operations of type 2 in PCAs
• Strictly primitive recursive realizability, I

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) First-order arithmetic and fragments (03F30)

Cites Work

• On the interpretation of intuitionistic number theory
• Title not available (Why is that?)
• On the computational content of the axiom of choice
• Classical logic as limit completion
• Relative Interpretations
• Towards the animation of proofs -- testing proofs by examples
• Models of arithmetic and recursive functions
• Limiting partial combinatory algebras
• Unitary Theories, Unitary Categories

Cited In (2)

• Title not available (Why is that?)
• Realizability models for a linear dependent PCF

This page was built for publication: Realizability interpretation of PA by iterated limiting PCA

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5740403)