Daniel Isaacson has advanced an epistemic notion of arithmetical truth according to which the latter is the set of truths that we grasp on the basis of our understanding of the structure of natural numbers alone. Isaacson’s thesis is then the claim that Peano Arithmetic (PA) is the theory of finite mathematics, in the sense that it proves all and only arithmetical truths thus understood. In this paper, we raise a challenge for the thesis and show how it can be (...) overcome. We introduce the concept of purity for theories of arithmetic: a theory of arithmetic is pure when it only proves arithmetical truths. Then, we argue that, under Isaacson’s thesis, some PA-provable truths—including transfinite induction claims for infinite ordinals and some consistency statements—are seemingly not arithmetical in Isaacson’s sense, and hence that Isaacson’s thesis might entail the impurity of PA. Nonetheless, we conjecture that the advocate of Isaacson’s thesis can avoid this undesirable consequence: the arithmetical nature, as understood by Isaacson, of all contentious PA-provable statements can be justified. As a case study, we explore how this is done for transfinite induction claims with infinite ordinals below ε0. To this end, we show that the PA-proof of such claims employs exclusively resources from finite mathematics, and that ordinals below ε0 are finitary objects despite being infinite. (shrink)

This book explains the first published consistency proof of PA. It contains the original Gentzen's proof, but it uses modern terminology and examples to illustrate the essential notions. The author comments on Gentzen's steps which are supplemented with exact calculations and parts of formal derivations. A notable aspect of the proof is the representation of ordinal numbers that was developed by Gentzen. This representation is analysed and connection to set-theoretical representation is found, namely an algorithm for translating Gentzen's notation into (...) Cantor normal form. The topic should interest researchers and students who work on proof theory, history of proof theory or Hilbert's program and who do not mind reading mathematical texts.​. (shrink)

Many efforts have been made in recent years to construct formal systems for mechanizing general mathematical reasoning. Most of these systems are based on logics which are stronger than first-order logic. However, there are good reasons to avoid using full second-order logic for this task. In this work we investigate a logic which is intermediate between FOL and SOL, and seems to be a particularly attractive alternative to both: ancestral logic. This is the logic which is obtained from FOL by (...) augmenting it with the transitive closure operator. While the study of this logic has so far been mostly model-theoretical, this work is devoted to its proof theory. Two natural Gentzen-style proof systems for ancestral logic are presented: one for the reflexive transitive closure, and one for the non-reflexive one. We show that these systems are sound for ancestral logic and provide evidence that they indeed encompass all forms of reasoning for this logic that are used in practice. The two systems are shown to be equivalent by providing translation algorithms between them. We end with an investigation of two main proof-theoretical properties: cut elimination and constructive consistency proof. (shrink)

Azriel Levy did fundamental work in set theory when it was transmuting into a modern, sophisticated field of mathematics, a formative period of over a decade straddling Cohen’s 1963 founding of forcing. The terms “Levy collapse”, “Levy hierarchy”, and “Levy absoluteness” will live on in set theory, and his technique of relative constructibility and connections established between forcing and definability will continue to be basic to the subject. What follows is a detailed account and analysis of Levy’s work and contributions (...) to set theory. (shrink)

This essay consists of two parts. In the first part, I focus my attention on the remarks that Frege makes on consistency when he sets about criticizing the method of creating new numbers through definition or abstraction. This gives me the opportunity to comment also a little on H. Hankel, J. Thomae—Frege’s main targets when he comes to criticize “formal theories of arithmetic” in Die Grundlagen der Arithmetik (1884) and the second volume of Grundgesetze der Arithmetik (1903)—G. Cantor, L. E. (...) J. Brouwer and D. Hilbert (1899). Part 2 is mainly devoted to Hilbert’s proof theory of the 1920s (1922–1931). I begin with an account of his early attempt to prove directly, and thus not by reduction or by constructing a model, the consistency of (a fragment of) arithmetic. In subsequent sections, I give a kind of overview of Hilbert’s metamathematics of the 1920s and try to shed light on a number of difficulties to which it gives rise. One serious difficulty that I discuss is the fact, widely ignored in the pertinent literature on Hilbert’s programme, that his language of finitist metamathematics fails to supply the conceptual resources for formulating a consistency statement qua unbounded quantification. Along the way, I shall comment on W. W. Tait’s objection to an interpretation of Hilbert’s finitism by Niebergall and Schirn, on G. Gentzen’s allegedly finitist consistency proof for Peano Arithmetic as well as his ideas on the provability and unprovability of initial cases of transfinite induction in pure number theory. Another topic I deal with is what has come to be known as partial realizations of Hilbert’s programme, chiefly advocated by S. G. Simpson. Towards the end of this essay, I take a critical look at Wittgenstein’s views about (in)consistency and consistency proofs in the period 1929–1933. I argue that both his insouciant attitude towards the emergence of a contradiction in a calculus and his outright repudiation of metamathematical consistency proofs are unwarranted. In particular, I argue that Wittgenstein falls short of making a convincing case against Hilbert’s programme. I conclude with some philosophical remarks on consistency proofs and soundness and raise a question concerning the consistency of analysis. (shrink)

Ratajczyk, Z., Subsystems of true arithmetic and hierarchies of functions, Annals of Pure and Applied Logic 64 95–152. The combinatorial method coming from the study of combinatorial sentences independent of PA is developed. Basing on this method we present the detailed analysis of provably recursive functions associated with higher levels of transfinite induction, I, and analyze combinatorial sentences independent of I. Our treatment of combinatorial sentences differs from the one given by McAloon [18] and gives more natural sentences. The same (...) method give also a combinatorial technique with no use of the cut-elimination theorem which is appropriate to study proof-theoretic strength of subsystems of first order arithmetic and some of their expansions. It was used to analyze iterated reflection principle and system of transfinite induction with a satisfaction class. (shrink)

We gather the following miscellaneous results in proof theory from the attic.1. 1. A provably well-founded elementary ordering admits an elementary order preserving map.2. 2. A simple proof of an elementary bound for cut elimination in propositional calculus and its applications to separation problem in relativized bounded arithmetic below S21.3. 3. Equivalents for Bar Induction, e.g., reflection schema for ω logic.4. 4. Direct computations in an equational calculus PRE and a decidability problem for provable inequations in PRE.5. 5. Intuitionistic fixed (...) point theories which are conservative extensions of HA.6. 6. Proof theoretic strengths of classical fixed points theories.7. 7. An equivalence between transfinite induction rule and iterated reflection schema over IΣn.8. 8. Derivation lengths of finite rewrite rules reducing under lexicographic path orders and multiply recursive functions.Each section can be read separately in principle. (shrink)

A proof of the consistency of Heyting arithmetic formulated in natural deduction is given. The proof is a reduction procedure for derivations of falsity and a vector assignment, such that each reduction reduces the vector. By an interpretation of the expressions of the vectors as ordinals each derivation of falsity is assigned an ordinal less than ε 0, thus proving termination of the procedure.

A variety of projects in proof theory of relevance to the philosophy of mathematics are surveyed, including Gödel's incompleteness theorems, conservation results, independence results, ordinal analysis, predicativity, reverse mathematics, speed-up results, and provability logics.

Exploiting the fact that -definable non-monotone inductive definitions have the same closure ordinal as arbitrary arithmetically definable monotone inductive definitions, we show that the proof theoretic ordinal of an axiomatization of -definable non-monotone inductive definitions coincides with the proof theoretic ordinal of the theory of arithmetically definable monotone inductive definitions.