The relative strengths of first-order theories axiomatized by transfinite induction, for ordinals less-than 0, and formulas restricted in quantifier complexity, is determined. This is done, in part, by describing the provably recursive functions of such theories. Upper bounds for the provably recursive functions are obtained using model-theoretic techniques. A variety of additional results that come as an application of such techniques are mentioned.

We apply Mints’ technique for proving the termination of the epsilon substitution method via cut-elimination to the system of Peano Arithmetic with Transfinite Induction given by Arai.

If α and β are ordinals, α ≤ β, and $\beta \nleq \alpha$ , then α + 1 ≤ β. The first result of this paper shows that the restriction of this statement to countable well orderings is provably equivalent to ACA 0 , a subsystem of second order arithmetic introduced by Friedman. The proof of the equivalence is reminiscent of Dekker's construction of a hypersimple set. An application of the theorem yields the equivalence of the set comprehension scheme ACA (...) 0 and an arithmetical transfinite induction scheme. (shrink)

We consider two variants of transfinite induction, one with monotonicity assumption on the predicate and one with the induction hypothesis only for cofinally many below. The latter can be seen as a transfinite analogue of the successor induction, while the usual transfinite induction is that of cumulative induction. We calculate the supremum of ordinals along which these schemata for \ formulae are provable in \. It is shown to be larger than the (...) proof-theoretic ordinal \ by power of base 2. We also show a similar result for the structural transfinite induction, defined with fundamental sequences. (shrink)

We prove the strong normalization theorem for the natural deduction system for the constructive arithmetic TRDB (the system with Definition by Transfinite Recursion and Bar induction), which was introduced by Yasugi and Hayashi. We also establish the consistency of this system, applying the strong normalization theorem.

Let T be a second-order arithmetical theory, Λ a well-order, λ < Λ and X ⊆ ℕ. We use $[\lambda |X]_T^{\rm{\Lambda }}\varphi$ as a formalization of “φ is provable from T and an oracle for the set X, using ω-rules of nesting depth at most λ”.For a set of formulas Γ, define predicative oracle reflection for T over Γ ) to be the schema that asserts that, if X ⊆ ℕ, Λ is a well-order and φ ∈ Γ, then$$\forall \,\lambda (...) < {\rm{\Lambda }}\,.$$In particular, define predicative oracle consistency ) as Pred–O–RFN{0=1}.Our main result is as follows. Let ATR0 be the second-order theory of Arithmetical Transfinite Recursion, ${\rm{RCA}}_0^{\rm{*}}$ be Weakened Recursive Comprehension and ACA be Arithmetical Comprehension with Full Induction. Then,$${\rm{ATR}}_0 \equiv {\rm{RCA}}_0^{\rm{*}} + {\rm{Pred - O - Cons\ }}\left \equiv {\rm{RCA}}_0^{\rm{*}} + \,{\rm{Pred - O - Cons\ }}\left \equiv {\rm{RCA}}_0^{\rm{*}} + \,{\rm{Pred - O - RFN}}\,_{{\bf{\Pi }}_2^1 } \left.$$We may even replace ${\rm{RCA}}_0^{\rm{*}}$ by the weaker ECA0, the second-order analogue of Elementary Arithmetic.Thus we characterize ATR0, a theory often considered to embody Predicative Reductionism, in terms of strong reflection and consistency principles. (shrink)

Handbook of Mathematical Induction: Theory and Applications shows how to find and write proofs via mathematical induction. This comprehensive book covers the theory, the structure of the written proof, all standard exercises, and hundreds of application examples from nearly every area of mathematics. In the first part of the book, the author discusses different inductive techniques, including well-ordered sets, basic mathematical induction, strong induction, double induction, infinite descent, downward induction, and several variants. He then (...) introduces ordinals and cardinals, transfinite induction, the axiom of choice, Zorn’s lemma, empirical induction, and fallacies and induction. He also explains how to write inductive proofs. The next part contains more than 750 exercises that highlight the levels of difficulty of an inductive proof, the variety of inductive techniques available, and the scope of results provable by mathematical induction. Each self-contained chapter in this section includes the necessary definitions, theory, and notation and covers a range of theorems and problems, from fundamental to very specialized. The final part presents either solutions or hints to the exercises. Slightly longer than what is found in most texts, these solutions provide complete details for every step of the problem-solving process. (shrink)

The starting point of this article is an old question asked by Feferman in his paper on Hancock's conjecture [6] about the strength of ${\rm ID}_{1}^{\ast}$. This theory is obtained from the well-known theory ID₁ by restricting fixed point induction to formulas that contain fixed point constants only positively. The techniques used to perform the proof-theoretic analysis of ${\rm ID}_{1}^{\ast}$ also permit to analyze its transfinitely iterated variants ${\rm ID}_{\alpha}^{\ast}$. Thus, we eventually know that $|\widehat{{\rm ID}}_{\alpha}|=|{\rm ID}_{\alpha}^{\ast}|$.

We show how Kreisel's representation theorem for sets in the analytical hierarchy can be generalized to sets defined by positive induction and use this to estimate the complexity of constructions in the theory of domains with totality.

ABSTRACT: It is argued that the equivalence, which is usually postulated to hold between infinite descent and transfinite induction in the foundations of arithmetic uses the law of excluded middle through the use of a double negation on the infinite set of natural numbers and therefore cannot be admitted in intuitionistic logic and mathematics, and a fortiori in more radical constructivist foundational schemes. Moreover it is shown that the infinite descent used in Dedekind-Peano arithmetic does not correspond to (...) the infinite descent of classical Fermatian arithmetic or number theory. However, from the point of view of classical logic, the principles of complete induction and transfinite induction, the least number principle and infinite descent are all equivalent. We find here a focal point for a foundational critique that aims for a a clarification of philosophical options in the foundations of logic and mathematics. (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)

Extending Gödel's Dialectica interpretation, we provide a functional interpretation of classical theories of positive arithmetic inductive definitions, reducing them to theories of finite-type functionals defined using transfinite recursion on well-founded trees.

We interpret intuitionistic theories of (iterated) strictly positive inductive definitions (s.p.-ID i′ s) into Martin-Löf's type theory. The main purpose being to obtain lower bounds of the proof-theoretic strength of type theories furnished with means for transfinite induction (W-type, Aczel's set of iterative sets or recursion on (type) universes). Thes.p.-ID i′ s are essentially the wellknownID i -theories, studied in ordinal analysis of fragments of second order arithmetic, but the set variable in the operator form is restricted to (...) occur only strictly positively. The modelling is done by constructivizing continuity notions for set operators at higher number classes and proving that strictly positive set operators are continuous in this sense. The existence of least fixed points, or more accurately, least sets closed under the operator, then easily follows. (shrink)

Some new double analogues of induction and transfinite recursion are given which yields a relatively simple proof of a result of Robert Cowen, [2] which in turn is a strengthening of an earlier result of Smullyan [1], which in turn gives a unified approach to Zorn's Lemma, the transfinite recursion theorem and certain results about ordinal numbers.

Let ≺ be a primitive recursive well-ordering on the natural numbers and assume that its order-type is greater than or equal to the proof-theoretic ordinal of the theory T. We show that the proof-theoretic strength of T is not increased if we add the negation of the statement which formalizes transfinite induction along ≺.

In the paper the problem of definability and undefinability of the concept of satisfaction and truth is considered. Connections between satisfaction and truth on the one hand and consistency of certain systems of omega-logic and transfinite induction on the other are indicated.

A principle, according to which any scientific theory can be mathematized, is investigated. Social science, liberal arts, history, and philosophy are meant first of all. That kind of theory is presupposed to be a consistent text, which can be exhaustedly represented by a certain mathematical structure constructively. In thus used, the term “theory” includes all hypotheses as yet unconfirmed as already rejected. The investigation of the sketch of a possible proof of the principle demonstrates that it should be accepted rather (...) a metamathematical axiom about the relation of mathematics and reality. The main statement is formulated as follows: Any scientific theory admits isomorphism to some mathematical structure in a way constructive. Its investigation needs philosophical means. Husserl’s phenomenology is what is used, and then the conception of “bracketing reality” is modelled to generalize Peano arithmetic in its relation to set theory in the foundation of mathematics. The obtained model is equivalent to the generalization of Peano arithmetic by means of replacing the axiom of induction with that of transfinite induction. The sketch of the proof is organized in five steps: a generalization of epoché; involving transfinite induction in the transition between Peano arithmetic and set theory; discussing the finiteness of Peano arithmetic; applying transfinite induction to Peano arithmetic; discussing an arithmetical model of reality. Accepting or rejecting the principle, two kinds of mathematics appear differing from each other by its relation to reality. Accepting the principle, mathematics has to include reality within itself in a kind of Pythagoreanism. These two kinds are called in paper correspondingly Hilbert mathematics and Gödel mathematics. The sketch of the proof of the principle demonstrates that the generalization of Peano arithmetic as above can be interpreted as a model of Hilbert mathematics into Gödel mathematics therefore showing that the former is not less consistent than the latter, and the principle is an independent axiom. The present paper follows a pathway grounded on Husserl’s phenomenology and “bracketing reality” to achieve the generalized arithmetic necessary for the principle to be founded in alternative ontology, in which there is no reality external to mathematics: reality is included within mathematics. That latter mathematics is able to self-found itself and can be called Hilbert mathematics in honour of Hilbert’s program for self-founding mathematics on the base of arithmetic. The principle of universal mathematizability is consistent to Hilbert mathematics, but not to Gödel mathematics. Consequently, its validity or rejection would resolve the problem which mathematics refers to our being; and vice versa: the choice between them for different reasons would confirm or refuse the principle as to the being. An information interpretation of Hilbert mathematics is involved. It is a kind of ontology of information. The Schrödinger equation in quantum mechanics is involved to illustrate that ontology. Thus the problem which of the two mathematics is more relevant to our being is discussed again in a new way A few directions for future work can be: a rigorous formal proof of the principle as an independent axiom; the further development of information ontology consistent to both kinds of mathematics, but much more natural for Hilbert mathematics; the development of the information interpretation of quantum mechanics as a mathematical one for information ontology and thus Hilbert mathematics; the description of consciousness in terms of information ontology. (shrink)

A principle, according to which any scientific theory can be mathematized, is investigated. That theory is presupposed to be a consistent text, which can be exhaustedly represented by a certain mathematical structure constructively. In thus used, the term “theory” includes all hypotheses as yet unconfirmed as already rejected. The investigation of the sketch of a possible proof of the principle demonstrates that it should be accepted rather a metamathematical axiom about the relation of mathematics and reality. Its investigation needs philosophical (...) means. Husserl’s phenomenology is what is used, and then the conception of “bracketing reality” is modelled to generalize Peano arithmetic in its relation to set theory in the foundation of mathematics. The obtained model is equivalent to the generalization of Peano arithmetic by means of replacing the axiom of induction with that of transfinite induction. A comparison to Mach’s doctrine is used to be revealed the fundamental and philosophical reductionism of Husserl’s phenomenology leading to a kind of Pythagoreanism in the final analysis. Accepting or rejecting the principle, two kinds of mathematics appear differing from each other by its relation to reality. Accepting the principle, mathematics has to include reality within itself in a kind of Pythagoreanism. These two kinds are called in paper correspondingly Hilbert mathematics and Gödel mathematics. The sketch of the proof of the principle demonstrates that the generalization of Peano arithmetic as above can be interpreted as a model of Hilbert mathematics into Gödel mathematics therefore showing that the former is not less consistent than the latter, and the principle is an independent axiom. An information interpretation of Hilbert mathematics is involved. It is a kind of ontology of information. Thus the problem which of the two mathematics is more relevant to our being is discussed. An information interpretation of the Schrödinger equation is involved to illustrate the above problem. (shrink)

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 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)

Gentzen’s approach by transfinite induction and that of intuitionist Heyting arithmetic to completeness and the self-foundation of mathematics are compared and opposed to the Gödel incompleteness results as to Peano arithmetic. Quantum mechanics involves infinity by Hilbert space, but it is finitist as any experimental science. The absence of hidden variables in it interpretable as its completeness should resurrect Hilbert’s finitism at the cost of relevant modification of the latter already hinted by intuitionism and Gentzen’s approaches for completeness. (...) This paper investigates both conditions and philosophical background necessary for that modification. The main conclusion is that the concept of infinity as underlying contemporary mathematics cannot be reduced to a single Peano arithmetic, but to at least two ones independent of each other. Intuitionism, quantum mechanics, and Gentzen’s approaches to completeness an even Hilbert’s finitism can be unified from that viewpoint. Mathematics may found itself by a way of finitism complemented by choice. The concept of information as the quantity of choices underlies that viewpoint. Quantum mechanics interpretable in terms of information and quantum information is inseparable from mathematics and its foundation. (shrink)

The proposition that a decreasing sequence of ordinals necessarily terminates has been given a new, and perhaps unexpected, importance by the rôle which it plays in Gentzen's proof of the freedom from contradiction of the “reine Zahlentheorie.” Gödel's construction of non-demonstrable propositions and the establishment of the impossibility of a proof of freedom from contradiction, within the framework of a certain type of formal system, showed that a proof of freedom from contradiction could be found only by transcending the axioms (...) and proof processes of that formal system. Gentzen's proof succeeds by utilisingtransfinite inductionto prove that certain sequences of reduction processes, enumerated by ordinals less than ε (the first ordinal to satisfy ε = ὡ) are finite. Were it possible to provethe restricted ordinal theorem, that a descending sequence of ordinals, less thanε, is finite, in Gentzen's “reine Zahlentheorie,” then it would be possible to determine a contradiction in that number system. In his paper, Gentzen proves the theorem of transfinite induction, which he requires, by an intuitive argument. There is also a method of reducing transfinite induction, for ordinals less than ε, to a number-theoretic principle given by Hilbert and Bernays, and a similar method by Ackermann. None of these proofs of transfinite induction isfinitist. (shrink)

Proof-theoretic reflection principles are schemas which attempt to express the soundness of arithmetical theories within their own language, e.g., ${\mathtt{{Prov}_{\mathsf {PA}} \rightarrow \varphi }}$ can be understood to assert that any statement provable in Peano arithmetic is true. It has been repeatedly suggested that justification for such principles follows directly from acceptance of an arithmetical theory $\mathsf {T}$ or indirectly in virtue of their derivability in certain truth-theoretic extensions thereof. This paper challenges this consensus by exploring relationships between reflection principles (...) and principles of mathematical and transfinite induction as well as the status of the latter with respect to various foundational characterizations of number theory. (shrink)

This paper offers an elementary proof that formal arithmetic is consistent. The system that will be proved consistent is a first-order theory R♯, based as usual on the Peano postulates and the recursion equations for + and ×. However, the reasoning will apply to any axiomatizable extension of R♯ got by adding classical arithmetical truths. Moreover, it will continue to apply through a large range of variation of the un- derlying logic of R♯, while on a simple and straightforward translation, (...) the classical first-order theory P♯ of Peano arithmetic turns out to be an exact subsystem of R♯. Since the reasoning is elementary, it is formalizable within R♯ itself; i.e., we can actually demonstrate within R♯ (or within P♯, if we care) a statement that, in a natural fashion, asserts the consistency of R♯ itself. The reader is unlikely to have missed the significance of the remarks just made. In plain English, this paper repeals Goedel’s famous second theorem. (That’s the one that asserts that sufficiently strong systems are inadequate to demonstrate their own consistency.) That theorem (or at least the significance usually claimed for it) was a mis- take—a subtle and understandable mistake, perhaps, but a mistake nonetheless. Accordingly, this paper reinstates the formal program which is often taken to have been blasted away by Goedel’s theorems— namely, the Hilbert program of demonstrating, by methods that everybody can recognize as effective and finitary, that intuitive mathematics is reliable. Indeed, the present consistency proof for arithmetic will be recognized as correct by anyone who can count to 3. (So much, indeed, for the claim that the reliability of arithmetic rests on transfinite induction up to ε0, and for the incredible mythology that underlies it.). (shrink)

Hilbert proposed the epsilon substitution method as a basis for consistency proofs. Hilbert's Ansatz for finding a solving substitution for any given finite set of transfinite axioms is, starting with the null substitution S0, to correct false values step by step and thereby generate the process S0,S1,… . The problem is to show that the approximating process terminates. After Gentzen's innovation, Ackermann 162) succeeded to prove termination of the process for first order arithmetic. Inspired by G. Mints as an (...) Ariadne's thread we formulate the epsilon substitution method for the theory ID1 of non-iterated inductive definitions for disjunctions of simply universal and existential operators, and give a termination proof of the H-process based on Ackermann 162). The termination proof is based on transfinite induction up to the Howard ordinal. (shrink)

In the 1920s, David Hilbert proposed a research program with the aim of providing mathematics with a secure foundation. This was to be accomplished by first formalizing logic and mathematics in their entirety, and then showing---using only so-called finitistic principles---that these formalizations are free of contradictions. ;In the area of logic, the Hilbert school accomplished major advances both in introducing new systems of logic, and in developing central metalogical notions, such as completeness and decidability. The analysis of unpublished material presented (...) in Chapter 2 shows that a completeness proof for propositional logic was found by Hilbert and his assistant Paul Bernays already in 1917--18, and that Bernays's contribution was much greater than is commonly acknowledged. Aside from logic, the main technical contribution of Hilbert's Program are the development of formal mathematical theories and proof-theoretical investigations thereof, in particular, consistency proofs. In this respect Wilhelm Ackermann's 1924 dissertation is a milestone both in the development of the Program and in proof theory in general. Ackermann gives a consistency proof for a second-order version of primitive recursive arithmetic which, surprisingly, explicitly uses a finitistic version of transfinite induction up to www . He also gave a faulty consistency proof for a system of second-order arithmetic based on Hilbert's &egr;-substitution method. Detailed analyses of both proofs in Chapter 3 shed light on the development of finitism and proof theory in the 1920s as practiced in Hilbert's school. ;In a series of papers, Charles Parsons has attempted to map out a notion of mathematical intuition which he also brings to bear on Hilbert's finitism. According to him, mathematical intuition fails to be able to underwrite the kind of intuitive knowledge Hilbert thought was attainable by the finitist. It is argued in Chapter 4 that the extent of finitistic knowledge which intuition can provide is broader than Parsons supposes. According to another influential analysis of finitism due to W. W. Tait, finitist reasoning coincides with primitive recursive reasoning. The acceptance of non-primitive recursive methods in Ackermann's dissertation presented in Chapter 3, together with additional textual evidence presented in Chapter 4, shows that this identification is untenable as far as Hilbert's conception of finitism is concerned. Tait's conception, however, differs from Hilbert's in important respects, yet it is also open to criticisms leading to the conclusion that finitism encompasses more than just primitive recursive reasoning. (shrink)

We formulate epsilon substitution method for theories (H)α0 of absolute jump hierarchies, and give two termination proofs of the H-process: The first proof is an adaption of Mints M, Mints-Tupailo-Buchholz MTB, i.e., based on a cut-elimination of a specially devised infinitary calculus. The second one is an adaption of Ackermann Ack. Each termination proof is based on transfinite induction up to an ordinal θ(α0+ ω)0, which is best possible.

In 1969, De Jongh proved the “maximality” of a fragment of intuitionistic predicate calculus forHA. Leivant strengthened the theorem in 1975, using proof-theoretical tools (normalisation of infinitary sequent calculi). By a refinement of De Jongh's original method (using Beth models instead of Kripke models and sheafs of partial combinatory algebras), a semantical proof is given of a result that is almost as good as Leivant's. Furthermore, it is shown thatHA can be extended to Higher Order Heyting Arithmetic+all trueΠ 2 0 (...) -sentences + transfinite induction over primitive recursive well-orderings. As a corollary of the proof, maximality of intuitionistic predicate calculus is established wrt. an abstract realisability notion defined over a suitable expansion ofHA. (shrink)

A constructivisation of the cut-elimination proof for sequent calculi for classical, intuitionistic and minimal infinitary logics with geometric rules—given in earlier work by the second author—is presented. This is achieved through a procedure where the non-constructive transfinite induction on the commutative sum of ordinals is replaced by two instances of Brouwer’s Bar Induction. The proof of admissibility of the structural rules is made ordinal-free by introducing a new well-founded relation based on a notion of embeddability of derivations. (...) Additionally, conservativity for classical over intuitionistic/minimal logic for the seven (finitary) Glivenko sequent classes is here shown to hold also for the corresponding infinitary classes. (shrink)