Annals of Pure and Applied Logic 55 (1):35-50 (1991)
AbstractWe prove that the theory IΔ0, extended by a weak version of the Δ0-Pigeonhole Principle, proves that every integer is the sum of four squares (Lagrange's theorem). Since the required weak version is derivable from the theory IΔ0 + ∀x (xlog(x) exists), our results give a positive answer to a question of Macintyre (1986). In the rest of the paper we consider the number-theoretical consequences of a new combinatorial principle, the ‘Δ0-Equipartition Principle’ (Δ0EQ). In particular we give a new proof, which can be formalized in IΔ0 + Δ0EQ, of the fact that every prime of the form 4n + 1 is the sum of two squares
Similar books and articles
Number theory and elementary arithmetic.Jeremy Avigad - 2003 - Philosophia Mathematica 11 (3):257-284.
Some nonstandard methods in combinatorial number theory.Steven C. Leth - 1988 - Studia Logica 47 (3):265 - 278.
A descriptive view of combinatorial group theory.Simon Thomas - 2011 - Bulletin of Symbolic Logic 17 (2):252-264.
On the philosophical significance of consistency proofs.Michael D. Resnik - 1974 - Journal of Philosophical Logic 3 (1/2):133 - 147.
Ramsey's Theorem for Pairs and Provably Recursive Functions.Alexander Kreuzer & Ulrich Kohlenbach - 2009 - Notre Dame Journal of Formal Logic 50 (4):427-444.
The equivalence of a generalized Martin's axiom to a combinatorial principle.William Weiss - 1981 - Journal of Symbolic Logic 46 (4):817-821.
An induction principle and pigeonhole principles for k-finite sets.Andreas Blass - 1995 - Journal of Symbolic Logic 60 (4):1186-1193.
A Formally Verified Proof of the Prime Number Theorem.Jeremy Avigad, Kevin Donnelly, David Gray & Paul Raff - 2007 - ACM Transactions on Computational Logic 9 (1).
Added to PP
Historical graph of downloads
Citations of this work
End extensions of models of linearly bounded arithmetic.Domenico Zambella - 1997 - Annals of Pure and Applied Logic 88 (2-3):263-277.
The prime number theorem and fragments ofP A.C. Cornaros & C. Dimitracopoulos - 1994 - Archive for Mathematical Logic 33 (4):265-281.
Quadratic forms in models of IΔ0+ Ω1. I.Paola D’Aquino & Angus Macintyre - 2007 - Annals of Pure and Applied Logic 148 (1):31-48.
Quadratic forms in models of I Δ 0 + Ω 1. I.Paola D’Aquino & Angus Macintyre - 2007 - Annals of Pure and Applied Logic 148 (1-3):31-48.
References found in this work
Existence and feasibility in arithmetic.Rohit Parikh - 1971 - Journal of Symbolic Logic 36 (3):494-508.
On the scheme of induction for bounded arithmetic formulas.A. J. Wilkie & J. B. Paris - 1987 - Annals of Pure and Applied Logic 35 (C):261-302.
Some Classes of Recursive Functions.Andrzej Grzegorczyk - 1955 - Journal of Symbolic Logic 20 (1):71-72.
Provability of the pigeonhole principle and the existence of infinitely many primes.J. B. Paris, A. J. Wilkie & A. R. Woods - 1988 - Journal of Symbolic Logic 53 (4):1235-1244.
Primes and their residue rings in models of open induction.Angus Macintyre & David Marker - 1989 - Annals of Pure and Applied Logic 43 (1):57-77.