Michael Rathjen

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.

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

The paper contains proof-theoretic investigation on extensions of Kripke-Platek set theory, KP, which accommodate first-order reflection. Ordinal analyses for such theories are obtained by devising cut elimination procedures for infinitary calculi of ramified set theory with Пn reflection rules. This leads to consistency proofs for the theories KP+Пn reflection using a small amount of arithmetic and the well-foundedness of a certain ordinal system with respect to primitive decending sequences. Regarding future work, we intend to avail ourselves of these new cut elimination techniques to attain an ordinal analysis of П12 comprehension by approaching П12 comprehension through transfinite levels of reflection.

While it is known that intuitionistic ZF set theory formulated with Replacement, IZFR, does not prove Collection, it is a longstanding open problem whether IZFR and intuitionistic set theory ZF formulated with Collection, IZF, have the same proof-theoretic strength. It has been conjectured that IZF proves the consistency of IZFR. This paper addresses similar questions but in respect of constructive Zermelo–Fraenkel set theory, CZF. It is shown that in the latter context the proof-theoretic strength of Replacement is the same as that of Strong Collection and also that the functional version of the Regular Extension Axiom is as strong as its relational version.Moreover, it is proved that, contrary to IZF, the strength of CZF increases if one adds an axiom asserting that the trichotomous ordinals form a set.Unlike IZF, constructive Zermelo–Fraenkel set theory is amenable to ordinal analysis and the proofs in this paper make pivotal use thereof in the guise of well-ordering proofs for ordinal representation systems

Constructive Zermelo–Fraenkel set theory, CZF, can be interpreted in Martin-Löf type theory via the so-called propositions-as-types interpretation. However, this interpretation validates more than what is provable in CZF. We now ask ourselves: is there a reasonably simple axiomatization of the set-theoretic formulae validated in Martin-Löf type theory? The answer is yes for a large collection of statements called the mathematical formulae. The validated mathematical formulae can be axiomatized by suitable forms of the axiom of choice.The paper builds on a self-interpretation of CZF IOS Press, Amsterdam, 2004 ]) that provides an “inner” model of CZF which also validates the so-called -axiom of choice, . The crucial technical step taken in the present paper is to investigate the absoluteness properties of this model under the hypothesis .It is also shown that CZF plus the -axiom of choice possesses the disjunction property, the numerical existence property and the existence property for an important group of formulae

The larger project broached here is to look at the generally sentence “if X is well-ordered then f is well-ordered”, where f is a standard proof-theoretic function from ordinals to ordinals. It has turned out that a statement of this form is often equivalent to the existence of countable coded ω-models for a particular theory Tf whose consistency can be proved by means of a cut elimination theorem in infinitary logic which crucially involves the function f. To illustrate this theme, we prove in this paper that the statement “if X is well-ordered then εX is well-ordered” is equivalent to. This was first proved by Marcone and Montalban [Alberto Marcone, Antonio Montalbán, The epsilon function for computability theorists, draft, 2007] using recursion-theoretic and combinatorial methods. The proof given here is principally proof-theoretic, the main techniques being Schütte’s method of proof search [Kurt Schütte, Proof Theory, Springer-Verlag, Berlin, Heidelberg, 1977] and cut elimination for a fragment of.

The fact that “natural” theories, i.e. theories which have something like an “idea” to them, are almost always linearly ordered with regard to logical strength has been called one of the great mysteries of the foundation of mathematics. However, one easily establishes the existence of theories with incomparable logical strengths using self-reference . As a result, PA+Con is not the least theory whose strength is greater than that of PA. But still we can ask: is there a sense in which PA+Con is the least “natural” theory whose strength is greater than that of PA? In this paper we exhibit natural theories in strength strictly between PA and PA+Con by introducing a notion of slow consistency

In ordinal analysis of impredicative theories so-called collapsing functions are of central importance. Unfortunately, the definition procedure of these functions makes essential use of uncountable cardinals whereas the notation system that they call into being corresponds to a recursive ordinal. It has long been claimed that, instead, one should manage to develop such functions directly on the basis of admissible ordinals. This paper is meant to show how this can be done. Interpreting the collapsing functions as operating directly on admissible sets also renders a new and perspicuous approach to well-ordering proofs possible. MSC: 03F15, 03F35

Universes of types were introduced into constructive type theory by Martin-Löf [12]. The idea of forming universes in type theory is to introduce a universe as a set closed under a certain specified ensemble of set constructors, say $\mathcal{C}$ . The universe then “reflects” $\mathcal{C}$ .This is the first part of a paper which addresses the exact logical strength of a particular such universe construction, the so-called superuniverse due to Palmgren (cf. [16, 18, 19]).It is proved that Martin-Löf type theory with a superuniverse, termed MLS, is a system whose proof-theoretic ordinal resides strictly above the Feferman-Schütte ordinal $\Gamma_0$ but well below the Bachmann-Howard ordinal. Not many theories of strength between $\Gamma_0$ and the Bachmann-Howard ordinal have arisen. MLS provides a natural example for such a theory

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.

One objective of this paper is the determination of the proof-theoretic strength of Martin-Löf's type theory with a universe and the type of well-founded trees. It is shown that this type system comprehends the consistency of a rather strong classical subsystem of second order arithmetic, namely the one with Δ 2 1 comprehension and bar induction. As Martin-Löf intended to formulate a system of constructive (intuitionistic) mathematics that has a sound philosophical basis, this yields a constructive consistency proof of a strong classical theory. Also the proof-theoretic strength of other inductive types like Aczel's type of iterative sets is investigated in various contexts.Further, we study metamathematical relations between type theories and other frameworks for formalizing constructive mathematics, e.g. Aczel's set theories and theories of operations and classes as developed by Feferman

KPM is a subsystem of set theory designed to formalize a recursively Mahlo universe of sets. In this paper we show that a certain ordinal notation system is sufficient to measure the proof-theoretic strength ofKPM. This involves a detour through an infinitary calculus RS(M), for which we prove several cutelimination theorems. Full cut-elimination is available for derivations of $\Sigma (L_{\omega _1^c } )$ sentences, whereω 1 c denotes the least nonrecursive ordinal. This paper is self-contained, at least from a technical point of view

Universes of types were introduced into constructive type theory by Martin-Löf [3]. The idea of forming universes in type theory is to introduce a universe as a set closed under a certain specified ensemble of set constructors, say ?. The universe then “reflects”?.This is the second part of a paper which addresses the exact logical strength of a particular such universe construction, the so-called superuniverse due to Palmgren (cf.[4–6]).It is proved that Martin-Löf type theory with a superuniverse, termed MLS, is a system whose proof-theoretic ordinal resides strictly above the Feferman-Schütte ordinal Γ0 but well below the Bachmann-Howard ordinal. Not many theories of strength between Γ0 and the Bachmann-Howard ordinal have arisen. MLS provides a natural example for such a theory. In this second part of the paper the concern is with the with upper bounds

In order to build the collection of Cauchy reals as a set in constructive set theory, the only power set-like principle needed is exponentiation. In contrast, the proof that the Dedekind reals form a set has seemed to require more than that. The main purpose here is to show that exponentiation alone does not suffice for the latter, by furnishing a Kripke model of constructive set theory, Constructive Zermelo–Fraenkel set theory with subset collection replaced by exponentiation, in which the Cauchy reals form a set while the Dedekind reals constitute a proper class

§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.

The context for this paper is Feferman's theory of explicit mathematics, T 0 . We address a problem that was posed in [6]. Let MID be the principle stating that any monotone operation on classifications has a least fixed point. The main objective of this paper is to show that T 0 + MID, when based on classical logic, also proves the existence of non-monotone inductive definitions that arise from arbitrary extensional operations on classifications. From the latter we deduce that MID, when adjoined to classical T 0 , leads to a much stronger theory than T 0

The context for this paper is Feferman's theory of explicit mathematics, a formal framework serving many purposes. It is suitable for representing Bishop-style constructive mathematics as well as generalized recursion, including direct expression of structural concepts which admit self-application. The object of investigation here is the theory of explicit mathematics augmented by the monotone fixed point principle, which asserts that any monotone operation on classifications (Feferman's notion of set) possesses a least fixed point. To be more precise, the new axiom not merely postulates the existence of a least solution, but, by adjoining a new functional constant to the language, it is ensured that a fixed point is uniformly presentable as a function of the monotone operation. The upshot of the paper is that the latter extension of explicit mathematics (when based on classical logic) embodies considerable proof-theoretic strength. It is shown that it has at least the strength of the subsystem of second order arithmetic based on Π 1 2 comprehension

This paper continues investigations of the monotone fixed point principle in the context of Feferman's explicit mathematics begun in [14]. Explicit mathematics is a versatile formal framework for representing Bishop-style constructive mathematics and generalized recursion theory. The object of investigation here is the theory of explicit mathematics augmented by the monotone fixed point principle, which asserts that any monotone operation on classifications (Feferman's notion of set) possesses a least fixed point. To be more precise, the new axiom not merely postulates the existence of a least solution, but, by adjoining a new constant to the language, it is ensured that a fixed point is uniformly presentable as a function of the monotone operation. Let T 0 + UMID denote this extension of explicit mathematics. [14] gave lower bounds for the strength of two subtheories of T 0 + UMID in relating them to fragments of second order arithmetic based on Π 1 2 comprehension. [14] showed that T $_0 \upharpoonright$ + UMID and T $_0 \upharpoonright$ + IND N + UMID have at least the strength of (Π 1 2 - CA) $\upharpoonright$ and (Π 1 2 - CA), respectively. Here we are concerned with the exact reversals. Let UMID N be the monotone fixed-point principle for subclassifications of the natural numbers. Among other results, it is shown that T $_0 \upharpoonright$ + UMID N and T $_0 \upharpoonright$ + IND N + UMID N have the same strength as (Π 1 2 - CA) $\upharpoonright$ and (Π 1 2 - CA), respectively. The results are achieved by constructing set-theoretic models for the aforementioned systems of explicit mathematics in certain extensions of Kripke-Platek set theory and subsequently relating these set theories to subsystems of second arithmetic