This book brings together philosophers, mathematicians and logicians to penetrate important problems in the philosophy and foundations of mathematics. In philosophy, one has been concerned with the opposition between constructivism and classical mathematics and the different ontological and epistemological views that are reflected in this opposition. The dominant foundational framework for current mathematics is classical logic and set theory with the axiom of choice. This framework is, however, laden with philosophical difficulties. One important alternative foundational programme that is actively pursued (...) today is predicativistic constructivism based on Martin-Löf type theory. Associated philosophical foundations are meaning theories in the tradition of Wittgenstein, Dummett, Prawitz and Martin-Löf. What is the relation between proof-theoretical semantics in the tradition of Gentzen, Prawitz, and Martin-Löf and Wittgensteinian or other accounts of meaning-as-use? What can proof-theoretical analyses tell us about the scope and limits of constructive and predicative mathematics? (shrink)

The Bachmann-Howard structure, that is the segment of ordinal numbers below the proof theoretic ordinal of Kripke-Platek set theory with infinity, is fully characterized in terms of CARLSON’s approach to ordinal notation systems based on the notion of Σ1-elementarity.

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)

We classify the phase transition thresholds from provability to unprovability for certain Friedman-style miniaturizations of Kruskal's Theorem and Higman's Lemma. In addition we prove a new and unexpected phase transition result for ε0. Motivated by renormalization and universality issues from statistical physics we finally state a universality hypothesis.

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.

Inspired by Pohlers' local predicativity approach to Pure Proof Theory and Howard's ordinal analysis of bar recursion of type zero we present a short, technically smooth and constructive strong normalization proof for Gödel's system T of primitive recursive functionals of finite types by constructing an ε 0 -recursive function [] 0 : T → ω so that a reduces to b implies [a] $_0 > [b]_0$ . The construction of [] 0 is based on a careful analysis of the Howard-Schütte (...) treatment of Gödel's T and utilizes the collapsing function ψ: ε 0 → ω which has been developed by the author for a local predicativity style proof-theoretic analysis of PA. The construction of [] 0 is also crucially based on ideas developed in the 1995 paper "A proof of strongly uniform termination for Gödel's T by the method of local predicativity" by the author. The results on complexity bounds for the fragments of T which are obtained in this paper strengthen considerably the results of the 1995 paper. Indeed, for given n let T n be the subsystem of T in which the recursors have type level less than or equal to n+2. (By definition, case distinction functionals for every type are also contained in T n .) As a corollary of the main theorem of this paper we obtain (reobtain?) optimal bounds for the T n -derivation lengths in terms of ω n+2 -descent recursive functions. The derivation lengths of type one functionals from T n (hence also their computational complexities) are classified optimally in terms of $ -descent recursive functions. In particular we obtain (reobtain?) that the derivation lengths function of a type one functional a ∈ T 0 is primitive recursive, thus any type one functional a in T 0 defines a primitive recursive function. Similarly we also obtain (reobtain?) a full classification of T 1 in terms of multiple recursion. As proof-theoretic corollaries we reobtain the classification of the IΣ n+1 -provably recursive functions. Taking advantage from our finitistic and constructive treatment of the terms of Gödel's T we reobtain additionally (without employing continuous cut elimination techniques) that PRA + PRWO ( $\varepsilon_0) \vdash \Pi^0_2$ - Refl(PA) and PRA + PRWO ( $\omega_{n+2}) \vdash \Pi^0_2$ - Refl(I Σ n+1 ), hence PRA + PRWO( $\epsilon_0) \vdash$ Con(PA) and PRA + PRWO( $\omega_{n+2}) \vdash$ Con(IΣ n+1 ). For programmatic reasons we outline in the introduction a vision of how to apply a certain type of infinitary methods to questions of finitary mathematics and recursion theory. We also indicate some connections between ordinals, term rewriting, recursion theory and computational complexity. (shrink)

This paper is intended to give for a general mathematical audience a survey of intriguing connections between analytic combinatorics and logic. We define the ordinals below ε0 in non-logical terms and we survey a selection of recent results about the analytic combinatorics of these ordinals. Using a versatile and flexible compression technique we give applications to phase transitions for independence results, Hilbert’s basis theorem, local number theory, Ramsey theory, Hydra games, and Goodstein sequences. We discuss briefly universality and renormalization issues (...) in this context. Finally, we indicate how regularity properties of ordinal count functions can be used to prove logical limit laws. (shrink)

For α less than ε0 let $N\alpha$ be the number of occurrences of ω in the Cantor normal form of α. Further let $\mid n \mid$ denote the binary length of a natural number n, let $\mid n\mid_h$ denote the h-times iterated binary length of n and let inv(n) be the least h such that $\mid n\mid_h \leq 2$ . We show that for any natural number h first order Peano arithmetic, PA, does not prove the following sentence: For all (...) K there exists an M which bounds the lengths n of all strictly descending sequences $\langle \alpha_0, ..., \alpha_n\rangle$ of ordinals less than ε0 which satisfy the condition that the Norm $N\alpha_i$ of the i-th term αi is bounded by $K + \mid i \mid \cdot \mid i\mid_h$ . As a supplement to this (refined Friedman style) independence result we further show that e.g., primitive recursive arithmetic, PRA, proves that for all K there is an M which bounds the length n of any strictly descending sequence $\langle \alpha_0,..., \alpha_n\rangle$ of ordinals less than ε0 which satisfies the condition that the Norm $N\alpha_i$ of the i-th term αi is bounded by $K + \mid i \mid\cdot inv(i)$ . The proofs are based on results from proof theory and techniques from asymptotic analysis of Polya-style enumerations. Using results from Otter and from Matou $\breve$ ek and Loebl we obtain similar characterizations for finite bad sequences of finite trees in terms of Otter's tree constant 2.9557652856... (shrink)

In this article we characterize a countable ordinal known as the big Veblen number in terms of natural well-partially ordered tree-like structures. To this end, we consider generalized trees where the immediate subtrees are grouped in pairs with address-like objects. Motivated by natural ordering properties, extracted from the standard notations for the big Veblen number, we investigate different choices for embeddability relations on the generalized trees. We observe that for addresses using one finite sequence only, the embeddability coincides with the (...) classical tree-embeddability, but in this article we are interested in more general situations. We prove that the maximal order type of some of these new embeddability relations hit precisely the big Veblen ordinal ϑΩΩ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\vartheta \Omega^{\Omega}}$$\end{document}. Somewhat surprisingly, changing a little bit the well-partially ordered addresses, the maximal order type hits an ordinal which exceeds the big Veblen number by far, namely ϑΩΩΩ\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$${\vartheta \Omega^{\Omega^\Omega}}$$\end{document}. Our results contribute to the research program on classifying properties of natural well-orderings in terms of order-theoretic properties of the functions generating the orderings. (shrink)

In reverse mathematics, it is possible to have a curious situation where we know that an implication does not reverse, but appear to have no information on how to weaken the assumption while preserving the conclusion (other than reducing all the way to the tautology of assuming the conclusion). A main cause of this phenomenon is the proof of a $\Pi^1_2$ sentence from the theory $\mathbf{\Pi^{\textbf{1}}_{\textbf{1}}-CA_{\textbf{0}}}$. Using methods based on the functional interpretation, we introduce a family of weakenings of $\mathbf{\Pi^{\textbf{1}}_{\textbf{1}}-CA_{\textbf{0}}}$ (...) and use them to give new upper bounds for the Nash-Williams Theorem of wqo theory and Menger's Theorem for countable graphs. (shrink)

In this article we investigate whether the following conjecture is true or not: does the addition-free theta functions form a canonical notation system for the linear versions of Friedman’s well-partial-orders with the so-called gap-condition over a finite set of n labels. Rather surprisingly, we can show this is the case for two labels, but not for more than two labels. To this end, we determine the order type of the notation systems for addition-free theta functions in terms of ordinals less (...) than ε0\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\varepsilon _0$$\end{document}. We further show that the maximal order type of the Friedman ordering can be obtained by a certain ordinal notation system which is based on specific binary theta functions. (shrink)

In recent years the question of whether adding the limited principle of omniscience, LPO, to constructive Zermelo–Fraenkel set theory, CZF, increases its strength has arisen several times. As the addition of excluded middle for atomic formulae to CZF results in a rather strong theory, i.e. much stronger than classical Zermelo set theory, it is not obvious that its augmentation by LPO would be proof-theoretically benign. The purpose of this paper is to show that CZF+RDC+LPO has indeed the same strength as (...) CZF, where RDC stands for relativized dependent choice. In particular, these theories prove the same Π02 theorems of arithmetic. (shrink)

We introduce and analyze two theories for typed inductive definitions and establish their proof-theoretic ordinal to be the small Veblen ordinal \. We investigate on the one hand the applicative theory \ of functions, inductive definitions, and types. It includes a simple type structure and is a natural generalization of S. Feferman’s system \\). On the other hand, we investigate the arithmetical theory \ of typed inductive definitions, a natural subsystem of \, and carry out a wellordering proof within \ (...) that makes use of fundamental sequences for ordinal notations in an ordinal notation system based on the finitary Veblen functions. The essential properties for describing the ordinal notation system are worked out. (shrink)

We present a list of open questions in reverse mathematics, including some relevant background information for each question. We also mention some of the areas of reverse mathematics that are starting to be developed and where interesting open question may be found.

§1. Introduction. A linear ordering embedsinto another linear ordering if it is isomorphic to a subset of it. Two linear orderings are said to beequimorphicif they can be embedded in each other. This is an equivalence relation, and we call the equivalence classesequimorphism types. We analyze the structure of equimorphism types of linear orderings, which is partially ordered by the embeddability relation. Our analysis is mainly fromthe viewpoints of Computability Theory and Reverse Mathematics. But we also obtain results, as the (...) definition of equimorphism invariants for linear orderings, which provide a better understanding of the shape of this structure in general.This study of linear orderings started by analyzing the proof-theoretic strength of a theorem due to Jullien [Jul69]. As is often the case in Reverse Mathematics, to solve this problem it was necessary to develop a deeper understanding of the objects involved. This led to a variety of results on the structure of linear orderings and the embeddability relation on them. These results can be divided into three groups. (shrink)

We prove Fraïssé’s conjecture within the system of Π11-comprehension. Furthermore, we prove that Fraïssé’s conjecture follows from the Δ20-bqo-ness of 3 over the system of Arithmetic Transfinite Recursion, and that the Δ20-bqo-ness of 3 is a Π21-statement strictly weaker than Π11-comprehension.

We say that a linear ordering is extendible if every partial ordering that does not embed can be extended to a linear ordering which does not embed either. Jullien’s theorem is a complete classification of the countable extendible linear orderings. Fraïssé’s conjecture, which is actually a theorem, is the statement that says that the class of countable linear ordering, quasiordered by the relation of embeddability, contains no infinite descending chain and no infinite antichain. In this paper we study the strength (...) of these two theorems from the viewpoint of Reverse Mathematics and Effective Mathematics. As a result of our analysis we get that they are equivalent over the basic system of .We also prove that Fraïssé’s conjecture is equivalent, over , to two other interesting statements. One that says that the class of well founded labeled trees, with labels from {+,−}, and with a very natural order relation, is well quasiordered. The other statement says that every linear ordering which does not contain a copy of the rationals is equimorphic to a finite sum of indecomposable linear orderings.While studying the proof theoretic strength of Jullien’s theorem, we prove the extendibility of many linear orderings, including ω2 and η, using just . Moreover, for all these linear orderings, , we prove that any partial ordering, , which does not embed has a linearization, hyperarithmetic in , which does not embed. (shrink)

We prove that the maximal order type of the wqo of linear orders of finite Hausdorff rank under embeddability is φ2, the first fixed point of the ε-function. We then show that Fraïssé’s conjecture restricted to linear orders of finite Hausdorff rank is provable in +“φ2 is well-ordered” and, over , implies +“φ2 is well-ordered”.

We consider five ordinal notation systems of ε0 which are all well-known and of interest in proof-theoretic analysis of Peano arithmetic: Cantor’s system, systems based on binary trees and on countable tree-ordinals, and the systems due to Schütte and Simpson, and to Beklemishev. The main point of this paper is to demonstrate that the systems except the system based on binary trees are equivalent as structured systems, in spite of the fact that they have their origins in different views and (...) trials in proof theory. This is true while Weiermann’s results based on Friedman-style miniaturization indicate that the system based on binary trees is of different character than the others. (shrink)

We have previously established that [Formula: see text]-comprehension is equivalent to the statement that every dilator has a well-founded Bachmann–Howard fixed point, over [Formula: see text]. In this paper, we show that the base theory can be lowered to [Formula: see text]. We also show that the minimal Bachmann–Howard fixed point of a dilator [Formula: see text] can be represented by a notation system [Formula: see text], which is computable relative to [Formula: see text]. The statement that [Formula: see text] (...) is well founded for any dilator [Formula: see text] will still be equivalent to [Formula: see text]-comprehension. Thus, the latter is split into the computable transformation [Formula: see text] and a statement about the preservation of well-foundedness, over a system of computable mathematics. (shrink)

It is generally accepted that H. Friedman’s gap condition is closely related to iterated collapsing functions from ordinal analysis. But what precisely is the connection? We offer the following answer: In a previous paper we have shown that the gap condition arises from an iterative construction on transformations of partial orders. Here we show that the parallel construction for linear orders yields familiar collapsing functions. The iteration step in the linear case is an instance of a general construction that we (...) call ‘Bachmann–Howard derivative’. In the present paper, we focus on the unary case, i.e., on the gap condition for sequences rather than trees and, correspondingly, on addition-free ordinal notation systems. This is partly for convenience, but it also allows us to clarify a phenomenon that is specific to the unary setting: As shown by van der Meeren, Rathjen and Weiermann, the gap condition on sequences admits two linearizations with rather different properties. We will see that these correspond to different recursive constructions of sequences. (shrink)

We present a new manifestation of Gödel’s second incompleteness theorem and discuss its foundational significance, in particular with respect to Hilbert’s program. Specifically, we consider a proper extension of Peano arithmetic ( $\mathbf {PA}$ ) by a mathematically meaningful axiom scheme that consists of $\Sigma ^0_2$ -sentences. These sentences assert that each computably enumerable ( $\Sigma ^0_1$ -definable without parameters) property of finite binary trees has a finite basis. Since this fact entails the existence of polynomial time algorithms, it is (...) relevant for computer science. On a technical level, our axiom scheme is a variant of an independence result due to Harvey Friedman. At the same time, the meta-mathematical properties of our axiom scheme distinguish it from most known independence results: Due to its logical complexity, our axiom scheme does not add computational strength. The only known method to establish its independence relies on Gödel’s second incompleteness theorem. In contrast, Gödel’s theorem is not needed for typical examples of $\Pi ^0_2$ -independence (such as the Paris–Harrington principle), since computational strength provides an extensional invariant on the level of $\Pi ^0_2$ -sentences. (shrink)

It is a striking fact from reverse mathematics that almost all theorems of countable and countably representable mathematics are equivalent to just five subsystems of second order arithmetic. The standard view is that the significance of these equivalences lies in the set existence principles that are necessary and sufficient to prove those theorems. In this article I analyse the role of set existence principles in reverse mathematics, and argue that they are best understood as closure conditions on the powerset of (...) the natural numbers. (shrink)

A poset is well‐partially ordered (WPO) if all its linear extensions are well orders; the supremum of ordered types of these linear extensions is the length, of p. We prove that if the vertex set X is infinite, of cardinality κ, and the ordering ⩽ is the intersection of finitely many well partial orderings of X,, then, letting, with, denote the euclidian division by κ (seen as an initial ordinal) of the length of each corresponding poset: where denotes the least (...) initial ordinal greater than the ordinal. This inequality is optimal. This result answers questions of Forster. (shrink)