This article provides a detailed comparison between two systems of collapsing functions. These functions play a crucial role in proof theory, in the analysis of patterns of resemblance, and the analysis of maximal order types of well partial orders. The exact correspondence given here serves as a starting point for far reaching extensions of current results on patterns and well partial orders. © 2011 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim.

We will introduce a partial ordering $\preceq_1$ on the class of ordinals which will serve as a foundation for an approach to ordinal notations for formal systems of set theory and second-order arithmetic. In this paper we use $\preceq_1$ to provide a new characterization of the ubiquitous ordinal $\epsilon _{0}$.

Taking up ordinal notations derived from Skolem hull operators familiar in the field of infinitary proof theory we develop a toolkit of ordinal arithmetic that generally applies whenever ordinal structures are analyzed whose combinatorial complexity does not exceed the strength of the system of set theory. The original purpose of doing so was inspired by the analysis of ordinal structures based on elementarity invented by T.J. Carlson, see [T.J. Carlson, Elementary patterns of resemblance, Annals of (...) Pure and Applied Logic 108 19–77], [G. Wilken, Σ1-Elementarity and Skolem hull operators, Annals of Pure and Applied Logic 145 162–175], and [G. Wilken, Assignment of ordinals to patterns of resemblance, The Journal of Symbolic Logic ]. Within the arithmetical context laid bare in this work, the “-numbers” play a role analogous to the role epsilon numbers play in the ordinal arithmetic based on the notion of Cantor normal form. (shrink)

The class of all ordinal numbers can be partitioned into two subclasses in such a way that neither subclass contains an arithmetic progression of order type ω, where an arithmetic progression of order type τ means an increasing sequence of ordinal numbers γ r, δ ≠ 0.

There are two well‐known ways of doing arithmetic with ordinal numbers: the “ordinary” addition, multiplication, and exponentiation, which are defined by transfinite iteration; and the “natural” (or “Hessenberg”) addition and multiplication (denoted ⊕ and ⊗), each satisfying its own set of algebraic laws. In 1909, Jacobsthal considered a third, intermediate way of multiplying ordinals (denoted × ), defined by transfinite iteration of natural addition, as well as the notion of exponentiation defined by transfinite iteration of his multiplication, which (...) we denote. (Jacobsthal's multiplication was later rediscovered by Conway.) Jacobsthal showed these operations too obeyed algebraic laws. In this paper, we pick up where Jacobsthal left off by considering the notion of exponentiation obtained by transfinitely iterating natural multiplication instead; we shall denote this. We show that and that ; note the use of Jacobsthal's multiplication in the latter. We also demonstrate the impossibility of defining a “natural exponentiation” satisfying reasonable algebraic laws. (shrink)

This paper investigates provability and non-provability of well-foundedness of ordinal notations in weak theories of bounded arithmetic. We define a notion of well-foundedness on bounded domains. We show that T21 and S22 can prove the well-foundedness on bounded domains of the ordinal notations below 0 and Γ0. As a corollary, the class of polynomial local search problems, PLS, can be augmented with cost functions that take ordinal values below 0 and Γ0 without increasing the class PLS.

This paper investigates provability and non-provability of well-foundedness of ordinal notations in weak theories of bounded arithmetic. We define a notion of well-foundedness on bounded domains. We show that T21 and S22 can prove the well-foundedness on bounded domains of the ordinal notations below 0 and Γ0. As a corollary, the class of polynomial local search problems, PLS, can be augmented with cost functions that take ordinal values below 0 and Γ0 without increasing the class PLS.

Jäger, G., Fixed points in Peano arithmetic with ordinals, Annals of Pure and Applied Logic 60 119-132. This paper deals with some proof-theoretic aspects of fixed point theories over Peano arithmetic with ordinals. It studies three such theories which differ in the principles which are available for induction on the natural numbers and ordinals. The main result states that there is a natural theory in this framework which is a conservative extension of Peano arithmeti.

Any set x is uniquely specified by the graph of the membership relation on the set obtained by adjoining x to the transitive closure of x. Thus any operation on sets can be looked at as an operation on these graphs. We look at the operations of ordinal arithmetic of sets in this light. This turns out to be simplest for a modified ordinal arithmetic based on the Zermelo ordinals, instead of the usual von Neumann ordinals. (...) In this arithmetic, addition of sets corresponds to concatenating graphs, and multiplication corresponds to replacing each edge of a graph by a copy of another graph. Characterizations for the von Neumann case are also given. (shrink)

The “high school algebra” laws of exponentiation fail in the ordinal arithmetic of sets that generalizes the arithmetic of the von Neumann ordinals. The situation can be remedied by using an alternative arithmetic of sets, based on the Zermelo ordinals, where the high school laws hold. In fact the Zermelo arithmetic of sets is uniquely characterized by its satisfying the high school laws together with basic properties of addition and multiplication. We also show how in (...) both arithmetics the behavior of exponentiation depends on whether the empty set is an element of the base. (shrink)

Dynamic ordinal analysis is ordinal analysis for weak arithmetics like fragments of bounded arithmetic. In this paper we will define dynamic ordinals – they will be sets of number theoretic functions measuring the amount of sΠ b 1(X) order induction available in a theory. We will compare order induction to successor induction over weak theories. We will compute dynamic ordinals of the bounded arithmetic theories sΣ b n (X)−L m IND for m=n and m=n+1, n≥0. Different (...) dynamic ordinals lead to separation. In this way we will obtain several separation results between these relativized theories. We will generalize our results to further languages extending the language of bounded arithmetic. (shrink)

This paper uses the framework of reverse mathematics to analyze the proof theoretic content of several statements concerning multiplication of countable well-orderings. In particular, a division algorithm for ordinal arithmetic is shown to be equivalent to the subsystem ATR0.

We present an analogue of Gödel’s second incompleteness theorem for systems of second-order arithmetic. Whereas Gödel showed that sufficiently strong theories that are $\Pi ^0_1$ -sound and $\Sigma ^0_1$ -definable do not prove their own $\Pi ^0_1$ -soundness, we prove that sufficiently strong theories that are $\Pi ^1_1$ -sound and $\Sigma ^1_1$ -definable do not prove their own $\Pi ^1_1$ -soundness. Our proof does not involve the construction of a self-referential sentence but rather relies on ordinal analysis.

There are multiple formal characterizations of the natural numbers available. Despite being inter-derivable, they plausibly codify different possible applications of the naturals – doing basic arithmetic, counting, and ordering – as well as different philosophical conceptions of those numbers: structuralist, cardinal, and ordinal. Nevertheless, some influential philosophers of mathematics have argued for a non-egalitarian attitude according to which one of those characterizations is more “legitmate” in virtue of being “more basic” or “more fundamental”. This paper addresses two related (...) issues. First, we review some of these non-egalitarian arguments, lay out a laundry list of different, legitimate, notions of relative priority, and suggest that these arguments plausibly employ different such notions. Secondly, we argue that given a metaphysical-cum-epistemological gloss suggested by Frege’s foundationalist epistomology, the ordinals are plausibly more basic than the cardinals. This is just one orientation to relative priority one could take, however. Ultimately, we subscribe to an egalitarian attitude towards these formal characterizations: they are, in some sense, equally “legitimate”. (shrink)

There are multiple formal characterizations of the natural numbers available. Despite being inter-derivable, they plausibly codify different possible applications of the naturals – doing basic arithmetic, counting, and ordering – as well as different philosophical conceptions of those numbers: structuralist, cardinal, and ordinal. Some influential philosophers of mathematics have argued for a non-egalitarian attitude according to which one of those characterizations is ‘more basic’ or ‘more fundamental’ than the others. This paper addresses two related issues. First, we review (...) some of these non-egalitarian arguments, lay out a laundry list of different, legitimate, notions of relative priority, and suggest that these arguments plausibly employ different such notions. Secondly, we argue that given a metaphysical-cum-epistemological gloss suggested by Frege's foundationalist epistemology, the ordinals are plausibly more basic than the cardinals. This is just one orientation to relative priority one could take, however. Ultimately, we subscribe to an egalitarian attitude towards these formal characterizations: they are, in some sense, equally ‘legitimate’. (shrink)

Abstract.This paper is the second in a series of three culminating in an ordinal analysis of Π12-comprehension. Its objective is to present an ordinal analysis for the subsystem of second order arithmetic with Δ12-comprehension, bar induction and Π12-comprehension for formulae without set parameters. Couched in terms of Kripke-Platek set theory, KP, the latter system corresponds to KPi augmented by the assertion that there exists a stable ordinal, where KPi is KP with an additional axiom stating that (...) every set is contained in an admissible set. (shrink)

An approach to ordinal analysis is presented which is finitary, but highlights the semantic content of the theories under consideration, rather than the syntactic structure of their proofs. In this paper the methods are applied to the analysis of theories extending Peano arithmetic with transfinite induction and transfinite arithmetic hierarchies.

The first attempt at a systematic approach to axiomatic theories of truth was undertaken by Friedman and Sheard (Ann Pure Appl Log 33:1–21, 1987). There twelve principles consisting of axioms, axiom schemata and rules of inference, each embodying a reasonable property of truth were isolated for study. Working with a base theory of truth conservative over PA, Friedman and Sheard raised the following questions. Which subsets of the Optional Axioms are consistent over the base theory? What are the proof-theoretic strengths (...) of the consistent theories? The first question was answered completely by Friedman and Sheard; all subsets of the Optional Axioms were classified as either consistent or inconsistent giving rise to nine maximal consistent theories of truth.They also determined the proof-theoretic strength of two subsets of the Optional Axioms. The aim of this paper is to continue the work begun by Friedman and Sheard. We will establish the proof-theoretic strength of all the remaining seven theories and relate their arithmetic part to well-known theories ranging from PA to the theory of ${\Sigma^1_1}$ dependent choice. (shrink)

It is well-known that natural axiomatic theories are well-ordered by consistency strength. However, it is possible to construct descending chains of artificial theories with respect to consistency strength. We provide an explanation of this well-orderedness phenomenon by studying a coarsening of the consistency strength order, namely, the$\Pi ^1_1$reflection strength order. We prove that there are no descending sequences of$\Pi ^1_1$sound extensions of$\mathsf {ACA}_0$in this ordering. Accordingly, we can attach a rank in this order, which we call reflection rank, to any$\Pi (...) ^1_1$sound extension of$\mathsf {ACA}_0$. We prove that for any$\Pi ^1_1$sound theoryTextending$\mathsf {ACA}_0^+$, the reflection rank ofTequals the$\Pi ^1_1$proof-theoretic ordinal ofT. We also prove that the$\Pi ^1_1$proof-theoretic ordinal of$\alpha $iterated$\Pi ^1_1$reflection is$\varepsilon _\alpha $. Finally, we use our results to provide straightforward well-foundedness proofs of ordinal notation systems based on reflection principles. (shrink)

In 1936, Gerhard Gentzen published a proof of consistency for Peano Arithmetic using transfinite induction up to ε0, which was considered a finitistically acceptable procedure by both Gentzen and Paul Bernays. Gentzen’s method of arithmetising ordinals and thus avoiding the Platonistic metaphysics of set theory traces back to the 1920s, when Bernays and David Hilbert used the method for an attempted proof of the Continuum Hypothesis. The idea that recursion on higher types could be used to simulate the limit-building (...) in transfinite recursion seems to originate from Bernays. The main difficulty, which was already discovered in Gabriel Sudan’s nearly forgotten paper of 1927, was that measuring transfinite ordinals requires stronger methods than representing them. This paper presents a historical account of the idea of nominalistic ordinals in the context of the Hilbert Programme as well as Gentzen and Bernays’ finitary interpretation of transfinite induction. (shrink)

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)

In [2] T. J. Carlson introduces an approach to ordinal notation systems which is based on the notion of Σ₁-elementary substructure. We gave a detailed ordinal arithmetical analysis (see [7]) of the ordinal structure based on Σ₁-elementarity as defined in [2]. This involved the development of an appropriate ordinal arithmetic that is based on a system of classical ordinal notations derived from Skolem hull operators, see [6]. In the present paper we establish an effective (...) order isomorphism between the classical and the new system of ordinal notations using the results from [6] and [7]. Moreover, on the basis of a concept of relativization we develop mutual (relatively) elementary recursive assignments which are uniform with respect to the underlying relativization. (shrink)

Turing progressions have been often used to measure the proof-theoretic strength of mathematical theories: iterate adding consistency of some weak base theory until you “hit” the target theory. Turing progressions based on n-consistency give rise to a \ proof-theoretic ordinal \ also denoted \. As such, to each theory U we can assign the sequence of corresponding \ ordinals \. We call this sequence a Turing-Taylor expansion or spectrum of a theory. In this paper, we relate Turing-Taylor expansions of (...) sub-theories of Peano Arithmetic to Ignatiev’s universal model for the closed fragment of the polymodal provability logic \. In particular, we observe that each point in the Ignatiev model can be seen as Turing-Taylor expansions of formal mathematical theories. Moreover, each sub-theory of Peano Arithmetic that allows for a Turing-Taylor expansion will define a unique point in Ignatiev’s model. (shrink)

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.

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.

§1. Introduction. The purpose of this paper is, in general, to report the state of the art of ordinal analysis and, in particular, the recent success in obtaining an ordinal analysis for the system of-analysis, which is the subsystem of formal second order arithmetic, Z2, with comprehension confined to-formulae. The same techniques can be used to provide ordinal analyses for theories that are reducible to iterated-comprehension, e.g.,-comprehension. The details will be laid out in [28].Ordinal-theoretic proof (...) theory came into existence in 1936, springing forth from Gentzen's head in the course of his consistency proof of arithmetic. Gentzen fostered hopes that with sufficiently large constructive ordinals one could establish the consistency of analysis, i.e., Z2. Considerable progress has been made in proof theory since Gentzen's tragic death on August 4th, 1945, but an ordinal analysis of Z2is still something to be sought. However, for reasons that cannot be explained here,-comprehension appears to be the main stumbling block on the road to understanding full comprehension, giving hope for an ordinal analysis of Z2in the foreseeable future.Roughly speaking,ordinally informativeproof theory attaches ordinals in a recursive representation system to proofs in a given formal system; transformations on proofs to certain canonical forms are then partially mirrored by operations on the associated ordinals. Among other things, ordinal analysis of a formal system serves to characterize its provably recursive ordinals, functions and functionals and can yield both conservation and combinatorial independence results. (shrink)

In this paper, representational structures of arithmetical thinking, encoded in human minds, are described. On the basis of empirical research, it is possible to distinguish four types of mental number lines: the shortest mental number line, summation mental number lines, point-place mental number lines and mental lines of exact numbers. These structures may be treated as generative mechanisms of forming arithmetical representations underlying our numerical acts of reference towards cardinalities, ordinals and magnitudes. In the paper, the theoretical framework for a (...) formal model of mental arithmetical representations is constructed. Many competitive conceptions of the mental system responsible for our arithmetical thinking may be unified within the presented framework. The paradigm underlying our research may be interpreted philosophically as a neo-Kantian approach to modeling the mind’s representational structures. (shrink)

§1. Introduction. The purpose of this paper is, in general, to report the state of the art of ordinal analysis and, in particular, the recent success in obtaining an ordinal analysis for the system of -analysis, which is the subsystem of formal second order arithmetic, Z2, with comprehension confined to -formulae. The same techniques can be used to provide ordinal analyses for theories that are reducible to iterated -comprehension, e.g., -comprehension. The details will be laid out (...) in [28].Ordinal-theoretic proof theory came into existence in 1936, springing forth from Gentzen's head in the course of his consistency proof of arithmetic. Gentzen fostered hopes that with sufficiently large constructive ordinals one could establish the consistency of analysis, i.e., Z2. Considerable progress has been made in proof theory since Gentzen's tragic death on August 4th, 1945, but an ordinal analysis of Z2 is still something to be sought. However, for reasons that cannot be explained here, -comprehension appears to be the main stumbling block on the road to understanding full comprehension, giving hope for an ordinal analysis of Z2 in the foreseeable future.Roughly speaking, ordinally informative proof theory attaches ordinals in a recursive representation system to proofs in a given formal system; transformations on proofs to certain canonical forms are then partially mirrored by operations on the associated ordinals. Among other things, ordinal analysis of a formal system serves to characterize its provably recursive ordinals, functions and functionals and can yield both conservation and combinatorial independence results. (shrink)

The paper establishes the general structure of the inconsistent models of arithmetic of [7]. It is shown that such models are constituted by a sequence of nuclei. The nuclei fall into three segments: the first contains improper nuclei: the second contains proper nuclei with linear chromosomes: the third contains proper nuclei with cyclical chromosomes. The nuclei have periods which are inherited up the ordering. It is also shown that the improper nuclei can have the order type of any (...) class='Hi'>ordinal, of the rationals, or of any other order type that can be embedded in the rationals in a certain way. (shrink)

Ordinal analysis is a research program wherein recursive ordinals are assigned to axiomatic theories. According to conventional wisdom, ordinal analysis measures the strength of theories. Yet what is the attendant notion of strength? In this paper we present abstract characterizations of ordinal analysis that address this question. -/- First, we characterize ordinal analysis as a partition of $\Sigma^1_1$-definable and $\Pi^1_1$-sound theories, namely, the partition whereby two theories are equivalent if they have the same proof-theoretic ordinal. (...) We show that no equivalence relation $\equiv$ is finer than the ordinal analysis partition if both: (1) $T\equiv U$ whenever $T$ and $U$ prove the same $\Pi^1_1$ sentences; (2) $T\equiv T+U$ for every set $U$ of true $\Sigma^1_1$ sentences. In fact, no such equivalence relation makes a single distinction that the ordinal analysis partition does not make. -/- Second, we characterize ordinal analysis as an ordering on arithmetically-definable and $\Pi^1_1$-sound theories, namely, the ordering wherein $T\leq U$ if the proof-theoretic ordinal of $T$ is less than or equal to the proof-theoretic ordinal of $U$. The standard ways of measuring the strength of theories are consistency strength and inclusion of $\Pi^0_1$ theorems. We introduce analogues of these notions---$\Pi^1_1$-reflection strength and inclusion of $\Pi^1_1$ theorems---in the presence of an oracle for $\Sigma^1_1$ truths, and prove that they coincide with the ordering induced by ordinal analysis. (shrink)

We study elementary second order extensions of the theoryID 1 of non-iterated inductive definitions and the theoryPA Ω of Peano arithmetic with ordinals. We determine the exact proof-theoretic strength of those extensions and their natural subsystems, and we relate them to subsystems of analysis with arithmetic comprehension plusΠ 1 1 comprehension and bar induction without set parameters.

We use model-theoretic methods described in [3] to obtain ordinal analyses of a number of theories of first-and second-order arithmetic, whose proof-theoretic ordinals are less than or equal to $\Gamma_0$.

We show that the categoricity of second-order Peano axioms can be proved from the comprehension axioms. We also show that the categoricity of second-order Zermelo–Fraenkel axioms, given the order type of the ordinals, can be proved from the comprehension axioms. Thus these well-known categoricity results do not need the so-called “full” second-order logic, the Henkin second-order logic is enough. We also address the question of “consistency” of these axiom systems in the second-order sense, that is, the question of existence of (...) models for these systems. In both cases we give a consistency proof, but naturally we have to assume more than the mere comprehension axioms. (shrink)

Elementary patterns of resemblance notate ordinals up to the ordinal of Pi^1_1-CA_0. We provide ordinal multiplication and exponentiation algorithms using these notations.

In his monograph On Numbers and Games, J. H. Conway introduced a real-closed field containing the reals and the ordinals as well as a great many less familiar numbers including $-\omega, \,\omega/2, \,1/\omega, \sqrt{\omega}$ and $\omega-\pi$ to name only a few. Indeed, this particular real-closed field, which Conway calls No, is so remarkably inclusive that, subject to the proviso that numbers—construed here as members of ordered fields—be individually definable in terms of sets of NBG, it may be said to contain (...) “All Numbers Great and Small.” In this respect, No bears much the same relation to ordered fields that the system ℝ of real numbers bears to Archimedean ordered fields. In Part I of the present paper, we suggest that whereas $\mathbb{R}$should merely be regarded as constituting an arithmetic continuum, No may be regarded as a sort of absolute arithmetic continuum, and in Part II we draw attention to the unifying framework No provides not only for the reals and the ordinals but also for an array of non-Archimedean ordered number systems that have arisen in connection with the theories of non-Archimedean ordered algebraic and geometric systems, the theory of the rate of growth of real functions and nonstandard analysis. In addition to its inclusive structure as an ordered field, the system No of surreal numbers has a rich algebraico-tree-theoretic structure—a simplicity hierarchical structure—that emerges from the recursive clauses in terms of which it is defined. In the development of No outlined in the present paper, in which the surreals emerge vis-à-vis a generalization of the von Neumann ordinal construction, the simplicity hierarchical features of No are brought to the fore and play central roles in the aforementioned unification of systems of numbers great and small and in some of the more revealing characterizations of No as an absolute continuum. (shrink)

This paper presents several proof-theoretic results concerning weak fixed point theories over second order number theory with arithmetic comprehension and full or restricted induction on the natural numbers. It is also shown that there are natural second order theories which are proof-theoretically equivalent but have different proof-theoretic ordinals.

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.