Hostname: page-component-78c5997874-8bhkd Total loading time: 0 Render date: 2024-11-19T06:29:15.975Z Has data issue: false hasContentIssue false
  • English
  • Français

Realizability interpretation of PA by iterated limiting PCA

Published online by Cambridge University Press:  11 March 2014

YOHJI AKAMA
YOHJI AKAMA*
Affiliation:
Mathematical Institute, Tohoku University, Aoba, Sendai, 980-8578Japan Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

For any partial combinatory algebra (PCA for short) $\mathcal{A}$, the class of $\mathcal{A}$-representable partial functions from $\mathbb{N}$ to $\mathcal{A}$ quotiented by the filter of cofinite sets of $\mathbb{N}$ is a PCA such that the representable partial functions are exactly the limiting partial functions of $\mathcal{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 Σ0n-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’.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 24 , Issue 6 , December 2014 , e240603
Copyright
Copyright © Cambridge University Press 2014 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Akama, Y. (2004) Limiting partial combinatory algebras. Theoretical Computer Science 311 (1–3)199–220.CrossRefGoogle Scholar
Akama, Y., Berardi, S., Hayashi, S. and Kohlenbach, U. (2004) An arithmetical hierarchy of the laws of excluded middle and related principles. In: Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science 192–201.CrossRefGoogle Scholar
Avigad, J. (2000) Realizability interpretation for classical arithmetic. In: Buss, S. R., Hájek, P. and Pudlk P. (eds.) Logic Colloquium '98, Lecture Notes in Logic 13, AK Peters57–90.Google Scholar
Beeson, M. J. (1985) Foundations of constructive mathematics, volume 6 of Ergebnisse der Mathematik und ihrer Grenzgebiete (3), Springer-Verlag.CrossRefGoogle Scholar
Berardi, S. (2005) Classical logic as limit completion. Mathematical Structures in Computer Science 15 (1)167–200.Google Scholar
Berardi, S., Bezem, M. and Coquand, T. (1998) On the computational content of the axiom of choice. Journal of Symbolic Logic 63 (2)600–622.Google Scholar
Hájek, P. and Pudlák, P. (1998) Metamathematics of first-order arithmetic (second printing), Perspectives in Mathematical Logic, Springer-Verlag.Google Scholar
Hayashi, S., Sumitomo, R. and Shii, K. (2002) Towards animation of proofs – testing proofs by examples. Theoretical Computer Science 272 (1–2)177–195.Google Scholar
Hindley, J. and Seldin, J. (1986) Introduction to Combinators and Lambda-calculus, Cambridge University Press.Google Scholar
Hirschfeld, J. (1975) Models of arithmetic and recursive functions. Israel Journal of Mathematics 20 (2)111–126.Google Scholar
Hofstra, P. and Cockett, R. (2010) Unitary theories, Unitary categories. Electronic Notes in Theoretical Computer Science 265 11–33.Google Scholar
Kleene, S. C. (1945) On the interpretation of intuitionistic number theory. Journal of Symbolic Logic 10 109–124.Google Scholar
Kleene, S. C. (1952) Introduction to metamathematics, Van Nostrand.Google Scholar
Lerman, M. (1970) Recursive functions modulo CO-r-maximal sets. Transactions of the American Mathematical Society 148 429–444.Google Scholar
Odifreddi, P. (1989) Classical Recursion Theory: The Theory of Functions and Sets of Natural Numbers, Studies in Logic and the Foundations of Mathematics 125, North-Holland.Google Scholar
Orey, S. (1961) Relative interpretations. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 7 146–153.Google Scholar
Smoryński, C. (1978) Nonstandard models of arithmetic. Course notes, fall 1978, Utrecht University. Logic group preprint series.Google Scholar
Smoryński, C. (1982) Nonstandard models and constructivity. In: Troelstra, A. and van Dalen, D. (eds.) The L. E. J. Brouwer Centenary Symposium (Noordwijkerhout, 1981), Studies in Logic and the Foundations of Mathematics 110, North-Holland459–464.CrossRefGoogle Scholar
Troelstra, A. S. (ed.) (1973) Metamathematical investigation of intuitionistic arithmetic and analysis. Springer-Verlag Lecture Notes in Mathematics 344.Google Scholar