Abstract
The first-order predicate calculus is complete for its intended semantics, by Gödel’s Completeness Theorem. Type Theory, though not complete for its intended semantics, is complete for the more liberal yet natural semantics of Henkin-structures. We derive here similar semantic characterizations for number theories.1 We show that Peano’s Arithmetic is sound and complete for truth (with object variables interpreted as natural numbers) in Henkin-structures that are closed under abstract jump (Theorem 4.10). By “abstract jump” we mean here Barwise’s strict-Π 11 definability, a notion that agrees with Turing jump over the natural numbers, and which we argue is of foundational significance. We also show that Σ1-Arithmetic is sound and complete for validity in all Henkin-structures that contain their “abstract RE” (i.e. strict- Π 11 definable) sets (Theorem 4.11). The paper is a refinement (of both results and exposition) of [Lei90]. The author is grateful to P. Odifreddi, J. Sgall, W. Sieg, and S. Simpson for useful comments and conversations pertaining to this paper.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Jon Barwise, Applications of strict- Π 11 predicates to infinitary logic, Journal of Symbolic Logic 34 (1969) 409–423.
Jon Barwise, “Admissible Sets and Structures”, Springer-Verlag, Berlin and New York, 1975.
Ronald Fagin , Generalized first order spectra and polynomial time recognizable sets, in R. Karp (ed.). “Complexity of Computation”, SIAM-AMS, 1974, 43–73.
Ronald Fagin, Monadic generalized spectra, Zeitschrift für mathematische Logik und Grundlagen der Mathematik 21 (1975) 89–96.
Harvey Friedman, König ’s Lemma is weak, Mimeographed note, Stanford University, 1969.
Haim Gaifman and Moshe Vardi, A simple proof that connectivity of finite graphs is not first-order definable, Bulletin of the EATCS 26 (June 1985) 43–45.
Leon Henkin, Completeness in the theory of types, Journal of Symbolic Logic 15 (1950) 81–91.
Neil Immerman, Languages which capture complexity classes, SIAM Journal of Computing 16 (1987) 760–778.
N.G. Jones and A.L. Selman, Turing machines and the spectra of first-order formulas, Journal of Symbolic Logic 39 (1974) 139–150.
S.C. Kleene, “Introduction to Metamathematics”, Wolterns-Noordhof, Groningen, 1952.
Phokion Kolaitis and Moshe Vardi, The decision problem for the probabilities of higher-order properties, Proceedings of the Nineteenth ACM Symposium on Theory of Computing, ACM, Providence, 1987, 425–435.
Phokion Kolaitis and Moshe Vardi, 0–1 laws and the decision problem for fragments of Second-Order Logic, Proceedings of the Third IEEE Symposium on Logic in Computer Science, IEEE, New York, 1988, 2–11.
Daniel Leivant , Logical and mathematical reasoning about programs, Conference Record of the Twelfth Annual Symposium on Principles of Programming Languages, ACM, New York, 1985, 132–140.
Daniel Leivant , Hoare’s logic captures program semantics, Manuscript, July 1985.
Daniel Leivant, Descriptive characterizations of computational complexity, Journal of Computer and System Sciences 39 (1989) 51–83.
Daniel Leivant, Computationally based set existence principles, in W. Sieg (ed.), “Logic and Computation”, Contemporary Mathematics, volume 106, American Mathematical Society, Providence, R.L, 1990, pp. 197–212.
Charles Parsons , On a number-theoretic choice schema and its relation to induction, in A. Kino et als. (eds.), “Intuitionism and Proof Theory”, North-Holland, Amsterdam, 1977, 459–473.
Dag Prawitz, “Natural Deduction”, Almqvist and Wiskel, Uppsala, 1965.
M. Presburger , Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt, Sprawozdanie z I Kongresu Matematików Krajów Slowianskich, (Comptes-rendus du Ier Congres des Mathématiciens des Pays Slaves), Warszawa 1929, Warsaw, 1930, pp. 92–101 and 395.
Wilfried Sieg , Provably recursive functionals of theories with König’s Lemma, Rend. Sem. Mat. Univers. Politecn. Torino, Fase. Specale: Logic and Computer Science (1986), 1987, 75–92.
Anne S. Troelstra , Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Springer-Verlag (LNM #344), Berlin, 1973.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1992 Springer-Verlag New York, Inc
About this paper
Cite this paper
Leivant, D. (1992). Semantic Characterizations of Number Theories. In: Moschovakis, Y.N. (eds) Logic from Computer Science. Mathematical Sciences Research Institute Publications, vol 21. Springer, New York, NY. https://doi.org/10.1007/978-1-4612-2822-6_12
Download citation
DOI: https://doi.org/10.1007/978-1-4612-2822-6_12
Publisher Name: Springer, New York, NY
Print ISBN: 978-1-4612-7685-2
Online ISBN: 978-1-4612-2822-6
eBook Packages: Springer Book Archive