An extended predicative definition of the Mahlo universe

Reinhard Kahle  Anton Setzer

CENTRIA and Departamento de Matemática Universidade Nova de Lisboa P–2829-516 Caparica, Portugal

                      kahle@mat.uc.pt

Department of Computer Science University of Wales Swansea Singleton Park Swansea SA2 8PP, UK

                   a.g.setzer@swan.ac.uk

Dedicated to Wolfram Pohlers on the occasion of his retirement

Abstract

In this article we develop a Mahlo universe in Explicit Mathematics using extended predicative methods. Our approach differs from the usual construction in type theory, where the Mahlo universe has a constructor that refers to all total functions from families of sets in the Mahlo universe into itself; such a construction is, in the absence of a further analysis, impredicative. By extended predicative methods we mean that universes are constructed from below, even if they have impredicative characteristics.

1 Predicativity^{1}

After the discovery of set theoretic paradoxes at the end of the 19th and beginning of the 20th century, especially Burali-Forti’s ([BF97]) and Russell’s (1901, [Rus02]), Russell [Rus06] introduced in 1906 the notion of predicativity. Poincaré (1906, [Poi06]) made this notion more precise and proposed a foundation of mathematics, which is entirely based on predicative constructions. A concept is called predicative, if its definition only refers to concepts introduced before and therefore does not presuppose its own existence. Many mathematical notions are introduced impredicatively. The most prominent example is the set of real numbers defined as Dedekind cuts.

Both authors were supported by the Volkswagen-Stiftung (RiP program at Oberwolfach). The first author was partially supported by the ESF research project Dialogical Foundations of Semantics within the ESF Eurocores program LogICCC (funded by the Portuguese Science Foundation, FCT LogICCC/0001/2007). The second author was supported by EPSRC grant EP/G033374/1, Theory and applications of induction-recursion.

1This historic introduction is partially based on [Fef05]

Hermann Weyl (1918, [Wey18]) was the first to carry out a systematic development of predicative mathematics. But it soon turned out that significant parts of established mathematics could not be developed using predicative methods. Kreisel proposed in 1958 ([Kre60]) that ramified analysis RA^{∗}, autonomously iterated, should be considered as the limit of predicative analysis. Using proof theoretic methods Kurt Schütte [Sch65b, Sch65a] and Solomon Feferman [Fef64] determined (independently, in 1964-5) Γ_{0} as the autonomous ordinal of RA^{∗}. (See also Schütte’s book [Sch77, p. 220] for an excellent presentation and discussion of this result.) Therefore, in proof theory Γ_{0} is usually considered as the limit of predicativity. Because of this result, predicative analysis is rather weak compared to other, more commonly used mathematical theories (e.g., Zermelo-Fraenkel set theory or full analysis). Already the first substantially impredicative theory ID_{1} has a proof theoretic ordinal which is substantially stronger than Γ_{0}.

Before moving beyond Γ_{0}, one should note that the results of reverse mathematics show that a substantial portion of ordinary “mathematical theorems” can be proven in the theory ATR_{0}, Arithmetical Transfinite Recursion, a theory of strength Γ_{0}, i.e., a theory which is predicative in the proof theoretic sense (see e.g. [Sim99]). However, some mathematical theorems require an extension of ATR_{0}, called (Π_{1}^{1}-CA)_{0}, which (from a proof theoretic perspective) is substantially impredicative (it has the strength of finitely iterated inductive definitions ID_{<ω}).

For theories whose proof theoretic ordinal is greater than Γ_{0}, but which can nonetheless be analysed using predicative methods (especially without the use of collapsing functions), Gerhard Jäger introduced the notion of metapredicativity. The first metapredicative treatment is [Jäg80], the first published metapredicative treatments are [JKSS99] and [Str99].

One should note that there are different understandings of what can be considered as predicative. For instance, in Martin-Löf type theory, inductive and inductive-recursive definitions (the latter allows to define strictly positive universes) are in general considered as predicative, referring to an intuitive understanding of what is meant by a least set closed under certain monotone operators. With inductive-recursive definitions one reaches the strength of KPM ([DS03], Theorem 6.4.2 and Corollary 6.4.3). A Mahlo Universe has been proposed by the second author in [Set00] as a predicatively justified extension of Martin-Löf Type Theory that goes beyond even KPM. In this article we explain how a Mahlo universe can in fact be considered as a predicative construction.

The other extreme position regarding predicativity is the observation that the natural numbers as defined in Peano Arithmetic can be considered as impredicative: they are defined as the least set closed under zero and successor, where “least” is characterized by the induction principle, which refers to the totality of the natural numbers. So the natural numbers are defined by referring to the totality of natural numbers. See Edward Nelson [Nel86], Daniel Leivant [Lei94, Lei95], and Charles Parsons [Par92], where Parsons refers this to an observation by Michael Dummett (no citation given).

In this article we introduce an extended predicative version of the Mahlo universe in the context of Explicit Mathematics. The corresponding theory is impredicative using the proof theoretic understanding (i.e., it goes beyond Γ_{0}; we expect it to even exceed slightly the strength of KPM). A Mahlo universe M is usually defined as, roughly speaking, a collection of sets such that for every function f : M → M there exist a subuniverse sub f of the Mahlo universe closed under f which is an element of the Mahlo universe. Closure under f means that f : sub f → sub f. This definition of M is impredicative, since it refers to the set of total functions from M into itself, which refers to the totality of M.

Our goal is to introduce the Mahlo universe “from below” so that the definition has an extended predicative character. For this it we will refer to the collection of arbitrary, (possibly) partial functions (which is unproblematic from a predicative point of view). This collection is not directly available in Martin-Löf Type Theory but in Explicit Mathematics, a framework developed by Solomon Feferman and further explored by the group of Gerhard Jäger. Therefore we develop the extended predicative Mahlo universe within the framework of Explicit Mathematics.

2 Mahloness

Mahlo cardinals were introduced 1911 by Paul Mahlo ([Mah11, Mah12]). Mahlo cardinals are the first substantial step in the development of large cardinals beyond inaccessible cardinals (weakly inaccessible cardinals were introduced 1908 by Felix Hausdorff [Hau08]). A (weakly) Mahlo cardinal is a cardinal κ which is (weakly) inaccessible and such that the set of (weakly) inaccessible cardinals less than κ is stationary in κ, i.e., every closed unbounded set in κ contains a (weakly) inaccessible cardinal.

For the proof-theoretic analysis of subsystems of analysis, proof theory makes extensive use of the recursive analogues of large cardinals ([Poh96, Poh98]). The recursive analogue of a regular cardinal is an admissible or recursively regular ordinal κ, which is an ordinal closed under all κ-partial recursive functions. (See [Hin78], Def. VIII.2.1). Recursively inaccessible ordinals are recursively regular ordinals κ that are the κ^{th} recursively regular ordinal ([Hin78], Def. VIII.6.1). The recursive analogue of a Mahlo cardinal is a recursively Mahlo ordinal. An admissible ordinal κ is a recursively Mahlo ordinal ([Hin78], Def. VIII.6.7) if for all f : M → M, which are Mrecursive with parameters in M, there exists an admissible κ < M such that ∀α < κ.f(α) < κ. (If one replaces “admissible” by “recursively inaccessible” in this definition, one obtains an equivalent definition.) Recursively Mahlo sets are sets of the form L_{M} for recursively Mahlo ordinals M.

The theory of recursively regular ordinals is often developed in the context of Kripke-Platek set theory KP. KP was introduced by Richard Platek 1966 in his PhD thesis [Pla66] with a variant introduced independently 1964 by Saul Kripke [Kri64]. The book of Jon Barwise [Bar75] contains an excellent exposition of KP, with the historical background described in Notes I.2.7. In the context of KP, an admissible set ([Bar75], Def. II.1.1) is a transitive set a which is a model of KP, where, apart from closure under pair, union and Δ_{0}-separation, the main property is closure under Δ_{0}-collection: If

b ∈ a ∧ ∀x ∈ b.∃y ∈ a.φ(x, y)

then there exists c ∈ a such that

∀x ∈ b.∃y ∈ c.φ(x, y)

for any Δ_{0}-formula φ with parameters in a. Recursively inaccessible sets ([Bar75], Def. V.6.7) are admissible sets closed under the operation of stepping to the next admissible set. Recursively Mahlo sets ([Bar75], Exercise. V.7.25) are admissible sets ad_{Mahlo} such that for all Δ_{0} formulas φ(x, y, z⃗) and variables z⃗ such that

z⃗ ∈ ad_{Mahlo} ∧ ∀x ∈ ad_{Mahlo}.∃y ∈ ad_{Mahlo}.φ(x, y, z⃗)

there exists an admissible b ∈ ad_{Mahlo} such that

z⃗ ∈ b ∧ ∀x ∈ b.∃y ∈ b.φ(x, y, z⃗)

holds. Admissible, recursively inaccessible and recursively Mahlo ordinals are the supremum of the ordinals in an admissible, recursively inaccessible and recursively Mahlo set, respectively. Alternatively they are the ordinals α such that L_{α} is admissible, recursively inaccessible or recursively Mahlo, respectively.

The step towards an analysis of recursively Mahlo ordinals was an important step in the development of impredicative proof theory. The first step in impredicative proof theory was the analysis of one inductive definition by William Alvin Howard ([How72]) based on the Bachmann Ordinal (introduced by Heinz Bachmann, [Bac50]). Today, this line of research is continued by two schools in proof theory, one founded by Kurt Schütte (see [Sch77]) and one founded by Gaisi Takeuti (see [Tak87]). The latter one is based on ordinal diagrams which are closer to Gentzen’s original paper [Gen36]. The most productive researcher following this approach is Toshiyasu Arai who pushed it beyond (Π_{2}^{1}-CA) + (BI) [Ara96a, Ara96b, Ara97a, Ara97b, Ara00a, Ara00b, Ara03, Ara04].

In the other school, iterated inductive definitions were analysed, culminating in a complete analysis in the famous monograph [BFPS81] by Buchholz, Pohlers, Feferman and Sieg. With Gerhard Jäger’s dissertation [Jäg79] the focus shifted from the analysis of subsystems of analysis to the analysis of extensions of KPω which allowed a much more fine grained development of intermediate theories. Here KPω is KP plus the existence of the set of natural numbers. This turned out to be very successful with the analysis by Wolfram Pohlers and Gerhard Jäger in 1982 of the equivalent theories KPI, (Δ_{2}^{1} − CA) + (BI), and T_{0} in [JP82]. Here KPI is KPω plus axioms stating the inaccessibility of the set theoretic universe, (Δ_{2}^{1} − CA) + (BI) is the subsystem of analysis with comprehension (CA) restricted to Δ_{2}^{1}-formulas which is extended by bar induction BI, and T_{0} is a system of explicit mathematics discussed in Sect. 3. The article [JP82] concentrates on the upper bound; the lower bound is based on the embedding of T_{0} into (Δ_{2}^{1} − CA) + (BI) by Feferman [Fef79] and a well-ordering proof for T_{0} by Jäger [Jäg83]. A more direct well-ordering proof can be found in [BS83] and [BS88] by Wilfried Buchholz and Kurt Schütte. The state-of-the-art treatment technique for determining upper bounds is based on the simplified version of local predicativity by Buchholz [Buc92]. A constructive underpinning was obtained by the second author, by carrying out a proof theoretic analysis of Martin-Löf type theory [Set98], showing that it is slightly stronger than KPI (see as well independent work by Michael Rathjen and E. Griffor [GR94].)

The first significant step beyond inaccessibles which were in some sense two level inductive definitions, was taken by Michael Rathjen ([Rat90, Rat91, Rat94a]) with his analysis of KPM, i.e. KPω with the Mahloness of its universe, and a corresponding subsystem of analysis [Rat96]. The second author of this article introduced in [Set00] a Mahlo universe in Martin-Löf type theory and showed that its strength goes slightly beyond that of KPM. This provided a first constructive underpinning of this proof-theoretic development. Later Gerhard Jäger (e.g. [Jäg05]) introduced a Mahlo universe in Explicit Mathematics (T_{0}(M)), which we will revisit in Sect. 4.

The analysis of KPM was the main stepping stone for Rathjen to jump to an analysis of KPω with Π_{3}-reflection ([Rat92, Rat94b]) and later of (Π_{2}^{1}-CA) + (BI) ([Rat95, Rat05a, Rat05b]).

We look now to the rules and axioms for formulating Mahlo in Explicit Mathematics. There are two versions, internal Mahlo (T_{0}(M)^{+}), corresponding to having a universe in Explicit Mathematics having the Mahlo property, and external Mahlo (T_{0}(M)), corresponding to the fact that the overall collection of sets has the Mahlo property. We first focus on the internal Mahlo universe, and then indicate how to modify this in order to obtain the external Mahlo universe.

The first part is that a recursively Mahlo set is a recursively inaccessible set (remember that we could replace admissibles by recursively inaccessible sets). Recursively inaccessible sets correspond to universes closed under inductive generation, so in T_{0}(M)^{+} we demand for some constant M corresponding to the recursively Mahlo set ad_{Mahlo} that it is a universe which is closed under inductive generation (which would correspond in type theory to closure under the W-type, in subsystems of analysis to the formation of inductively defined sets, and in KP to the formation of the next admissible above a given set). We note here that the metapredicative versions are obtained by omitting inductive generation—which is an impredicative concept in the proof theoretic sense. Thus, for metapredicative Mahlo, closure under inductive generation is omitted.

The assumption for the main closure property of ad_{Mahlo} is z⃗ ∈ ad_{Mahlo} and ∀x ∈ ad_{Mahlo}.∃y ∈ ad_{Mahlo}.φ(x, y, z⃗). We can collect the elements z⃗ together into one set a and replace the closure under φ by a function f ∈ (M → M).

The reader with a background in Martin-Löf Type Theory might wonder why this is sufficient, since in type theory this assumption is translated as having a function f ∈ (Fam(M) → Fam(M)), where^{2}

Fam(u) := {(a, b) | a ˙∈ u ∧ b ∈ (a → u)} .

The reason why this can be avoided is that for any universe u we can write encoding functions pair ∈ (Fam(u) → u) and decoding functions proj_{0} ∈ (u → u) and proj_{1} ∈ ((x ˙∈ u) → proj_{0} x → u) for families of sets such that for a ˙∈ u and b ∈ (a → u) we have proj_{0} (pair (a, b)) ˙= a and proj_{1} (pair (a, b)) ˙= b. We use here notations inherited from dependent type theory, proj_{1} ∈ ((x ˙∈ u) → proj_{0} x → u) means that proj_{1} is a defined constant such that

∀x ˙∈ u.∀y ˙∈ proj_{0} x.proj_{1} x y ˙∈ u .

For this one defines (using join and arithmetic comprehension)

pair (a, b) := {(0, x) | x ˙∈ a} ∪ {(1, (x, y)) | x ˙∈ a ∧ y ˙∈ b x} ,
proj_{0} a := {x | (0, x) ˙∈ a} ,
proj_{1} a x := {y | (1, (x, y)) ˙∈ a} .

Now a function f ∈ (Fam(u) → Fam(u)) can be encoded as a function g ∈ (u → u) s.t. g x = pair (f (proj_{0} x, proj_{1} x)), and a universe u is closed under f if and only if it is closed under g (modulo ˙=). In the same way we can replace z⃗ occurring above, which would be translated into an element of Fam(u), by one single element of u.

Assuming the closure of ad_{Mahlo} under z⃗ and φ the recursively Mahlo property gave us the existence of a recursively inaccessible b containing z⃗ and closed under φ. The existence of b translates into the existence of a subuniverse m (a, f). So we have m (a, f) is a universe, m (a, f) ⊆ M. (Note that in type theory an explicit embedding from m (a, f) into M needs to be defined, which we can avoid in Explicit Mathematics because there universes are à la Russell rather than à la Tarski). z⃗ ∈ b translates into a ˙∈ m (a, f) and that ad_{Mahlo} is closed under φ is translated into f ∈ (m (a, f) → m (a, f)). (In type theory it was necessary to introduce a constructor reflecting f in m (a, f), which is implicit in Explicit Mathematics. Furthermore, in the formulation of the Mahlo universe in [Set00] the parameter a doesn’t occur. This is because closure under a can be avoided by replacing closure under f by closure under g such that g x is the union of f x and a.)

2The notations ˙∈, ˙=, ˙⊂, ℜ and related notions are introduced in Section 3, which introduces as well the theory T_{0}.

Universes in Explicit mathematics are usually not closed under inductive generation, and we follow this convention. We observe that M needs in addition to being a universe to be closed under inductive generation. However, m (a, f) does not need to be closed under inductive generation: We can use again the trick of encoding of families of sets into sets and define for every f ∈ (M → M) a function g ∈ (M → M) such that u is closed under g if u is closed under f and inductive generation (modulo ˙=). So we obtain that, even if m (a, f) is not necessarily closed under inductive generation, there still exists for every f ∈ (M → M) a subuniverse of M closed under f and inductive generation (modulo ˙=).

Up to now, the strength of the rules does not exceed possessing T_{0} plus the existence of one universe, since we could easily model m (a, f) := M. What is still missing is to model that the admissible is an element of M, which is modelled by

m (a, f) ˙∈ M

Note that this means that M has a constructor that depends negatively on M, namely

m ∈ ((M, (M → M)) → M)

This completes the internal version of the Mahlo universe, which can be summarized as follows (notations such as U(t) will be explained in the next section):

U(M) ∧ i ∈ (M^{2} → M)

a ˙∈ M ∧ f ∈ (M → M) → m (a, f) ˙⊂ M ∧ U(m (a, f)) ∧ a ˙∈ m (a, f)
a ˙∈ M ∧ f ∈ (M → M) → f ∈ (m (a, f) → m (a, f)) ∧ m (a, f) ˙∈ M

An external Mahlo universe is obtained by giving the collection ℜ of names for sets in Explicit Mathematics the rôle of M. So we obtain as conditions the axioms developed by Jäger (in addition to T_{0} which contains closure of ℜ under i):

ℜ(a) ∧ f ∈ (ℜ → ℜ) → U(m (a, f)) ∧ a ˙∈ m (a, f),
ℜ(a) ∧ f ∈ (ℜ → ℜ) → f ∈ (m (a, f) → m (a, f)).

3 Explicit Mathematics

We work in the framework of Feferman’s Explicit Mathematics, [Fef75, Fef79]. It was introduced in the 1970s to formalize Bishop-style constructive mathematics.

Explicit Mathematics is based on a two-sorted language, comprising individuals (combinatory logic plus additional constants) and types (i.e., collections of individuals). As general convention, individual constants are given as lower case letters (or letter combinations) in sans serif font, individual variables as roman lower case letters, such as x, y, individual terms as roman lower case letters such as r, s, t, and type variables in roman upper case letters such as U, V, X, Y (we do not use type constants). Types are named by individuals, which are formally expressed by a naming relation ℜ(x, U), and one has an axiom expressing that every type has a name:

∀U.∃x.ℜ(x, U).

Based on the primitive element relation t ∈ X, it is convenient to introduce the following abbreviations:

ℜ(s) := ∃X.ℜ(s, X),
s ˙∈ t := ∃X.ℜ(t, X) ∧ s ∈ X,
∃x ˙∈ s.φ(x) := ∃x.x ˙∈ s ∧ φ(x),
∀x ˙∈ s.φ(x) := ∀x.x ˙∈ s → φ(x),
s ˙⊂ t := ∀x ˙∈ s.x ˙∈ t,
s ˙= t := s ˙⊂ t ∧ t ˙⊂ s,
ℜ_{ℜ}(s) := ℜ(s) ∧ ∀x ˙∈ s.ℜ_{ℜ}(x),
f ∈ (ℜ → ℜ) := ∀x.ℜ(x) → ℜ(f x),
f ∈ (s → s) := ∀x.x ˙∈ s → f x ˙∈ s,
f ∈ (s^{2} → s) := ∀x, y.x ˙∈ s ∧ y ˙∈ s → f (x, y) ˙∈ s.

The usual starting point of Explicit Mathematics is the theory EETJ of explicit elementary types with join, cf. [FJ96]. It is based on Beeson’s classical logic of partial terms (see [Bee85] or [TvD88]) for individuals and classical logic for types. The first order part is given by applicative theories which formalize partial combinatory algebra, pairing and projection, and axiomatically introduced natural numbers, cf. [JKS99]. EETJ adds types on the second order level, and axiomatize elementary comprehension and join as type construction operations. We dispense here with a detailed description of EETJ which can be found in many papers on Explicit Mathematics (e.g., [JKS01], [JS02] or [Kah07]). Let us just briefly address the finite axiomatization of elementary comprehension and join. For these, we have the following individual constants in the language: nat (natural numbers), id (identity), co (complement), int (intersection), dom (domain), inv (inverse image), and j (join). These constants together make up a set of generators, to which also belong—depending on the particular theory under consideration—other constants used to introduce names, such as i (inductive generation) in T_{0} or m in the approaches to Mahlo; for the extended predicative version we have also the additional generators M, pre and sub. From the axiomatization we just give as an example the one for intersections:

ℜ(a) ∧ ℜ(b) → ℜ(int (a, b)) ∧ ∀x.x ˙∈ int (a, b) ↔ x ˙∈ a ∧ x ˙∈ b.

The generators for elementary comprehension and join will appear again below when we define the notion of universe in Explicit Mathematics as a type which is closed under elementary comprehension and join.

3.1 Inductive Generation

Let us shortly address the most famous theory of Explicit Mathematics, T_{0} [Fef75], which is obtained from EETJ by adding inductive generation and the standard induction scheme on natural numbers for arbitrary formulae of the language. Using the abbreviation

Closed(a, b, S) := ∀x ˙∈ a.(∀y ˙∈ a.(y, x) ˙∈ b → y ∈ S) → x ∈ S

inductive generation is given by the following two axioms, expressing that i (a, b) is the least fixed point of the operator X ↦ Closed(a, b, X), or the accessible part of the relation b restricted to a:^{3}

(IG.1) ℜ(a) ∧ ℜ(b) → ∃X.ℜ(i (a, b), X) ∧ Closed(a, b, X), (IG.2) ℜ(a) ∧ ℜ(b) ∧ Closed(a, b, φ) → ∀x ˙∈ i (a, b).φ(x).

As mentioned before, the theory T_{0} played an important role in the proof-theoretic analysis of the theories the proof theoretically equivalent theories (Δ_{2}^{1} − CA) + (BI) and KPI (see [Fef79, Jäg83]); since T_{0} has the same strength as KPI, one can say that inductive generation is a way of formalizing inaccessibility in Explicit Mathematics, and formalizing it “from below”.

3.2 Universes

We now turn to the notion of universes as discussed, for instance, in [JKS01]. In the context of Mahloness, universes are considered by Jäger, Strahm, and Studer [JS01, JS02, Str02, Jäg05, JS05].

The concept of universes can be introduced as a defined notion: A universe is a type W such that:

3Formulas such as Closed(a, b, φ) are to be understood in the obvious way (replace in Closed(a, b, S) formulas t ∈ S by φ(t)). This convention will apply later even to formulas where a name for a set a is replaced by φ – then s ˙∈ a is to be replaced by φ(s).

1. all elements of W are names and

2. W is closed under elementary comprehension and join.

For the formal definition we introduce the auxiliary notation of the closure condition C(W, a) as the disjunction of the following formulas:

(1) a = nat ∨ a = id,

(2) ∃x.a = co x ∧ x ∈ W,

(3) ∃x.∃y.a = int (x, y) ∧ x ∈ W ∧ y ∈ W,

(4) ∃x.a = dom x ∧ x ∈ W,

(5) ∃f.∃x.a = inv (f, x) ∧ x ∈ W,

(6) ∃x.∃f.a = j (x, f) ∧ x ∈ W ∧ ∀y ˙∈ x.f y ∈ W.

The formula ∀x.C(W, x) → x ∈ W expresses that W is a type closed under the type constructions of EETJ, i.e., elementary comprehension and join. Now, we define a universe as a collection of names which satisfies this closure condition, and we write U(W) to express that W is a universe:

U(W) := (∀x ∈ W.ℜ(x)) ∧ ∀x.C(W, x) → x ∈ W .

We write U(t) to express that t is a name of a universe:

U(t) := ∃X.ℜ(t, X) ∧ U(X).

A detailed discussion of the concept of universes in Explicit Mathematics can be found in [JKS01], including least universes and name induction. Universes can be considered as a formalization of admissibility. However, since, if one adds induction axioms expressing least universes or name induction, one reaches inacessibilty, they can serve as alternatives to inductive generation in T_{0}.

4 Axiomatic Mahlo

The first formulation of Mahlo in Explicit Mathematics was given in a metapredicative setting by Jäger and Strahm [JS01]. Its proof theoretic strength was determined in [Str02] (with the upper bound given in [JS01]) as φ ε_{0} 0 0 (with induction restricted to types the strength is φ ω 0 0). The non-metapredicative version, which is obtained by adding inductive generation, was studied by Jäger and Studer [JS02]. The resulting theory T_{0}(M)

(Explicit Mathematics with Mahlo) is defined as the extension of T_{0} by the following two axioms:

(M1)  ℜ(a) ∧ f ∈ (ℜ → ℜ) → U(m (a, f)) ∧ a ˙∈ m (a, f),
(M2)  ℜ(a) ∧ f ∈ (ℜ → ℜ) → f ∈ (m (a, f) → m (a, f)).

The axioms state that for every function from names to names there is a universe which is closed under f. This universe is defined uniformly in f by use of the universe constructor m.

An overview over what is known about T_{0}(M) can be found in Jäger’s article [Jäg05]. Together with Thomas Studer [JS02] he determined an upper bound for the proof theoretic strength of Explicit Mathematics with impredicative Mahlo, using specific nonmonotone inductive definitions introduced by Richter [Ric71], see also [Jäg01]. A lower bound can be combined according to Jäger [Jäg05] by using the realization of CZF with Mahloness into Explicit Mathematics with the Mahlo universe (Sergei Tupailo [Tup03]) together with a not-worked out adaption of the well-ordering proof by Michael Rathjen [Rat94a] for KPM:^{4}

Theorem. T_{0}(M) ≡ KPM and the proof-theoretic ordinal is Ψ_{Ω}(ε_{M_{0}+1}).

The axiomatization of the universe m (a, f) for a given function f (and given name a) is impredicative in the following sense: f is assumed to be a total function from names to names but this totality has to hold, of course, also with respect to the name of the “newly introduced” universe m (a, f). In other words, in order to verify the premise f ∈ (ℜ → ℜ) one already needs to “know” m (a, f).

We call this approach to Mahlo universes axiomatic.

Jäger and Studer, in [JS02], also consider a variant of T_{0}(M) which is based on partial functions, partial with respect to the definedness predicate of the underlying applicative theory. It is ease to see from the model construction that this does not change the proof-theoretic strength. Note that, when we speak about partiality of function in the following, we have something else in mind, namely that there are no “a priori” conditions given on the behaviour of a function outside of the subuniverse under consideration.

In the given form, T_{0}(M) axiomatizes an “external” Mahlo universe, in the sense that the “universe” of all names—the extension of ℜ—has the Mahlo property. However, the collections of all names is not a universe in the defined sense of the theory.

Tupailo [Tup03, p. 172, IX] also considers an extension of T_{0}, which he called T_{0} + M^{+}, which formalizes an “internal” Mahlo universe, i.e., there is a universe—in the sense defined within the theory—, named by M which has the Mahlo property. We formalise a variant T_{0}(M)^{+} which consists of the axioms of T_{0} plus the following axioms:

4The second author regards the latter as a good hint why this theorem is true, but details in well-ordering proofs can be quite tricky and more details need to be worked out before we can regard this result as a full theorem.

U(M) ∧ i ∈ (M^{2} → M), (M^{+}1)

(M^{+}2)  a ˙∈ M ∧ f ∈ (M → M) → m (a, f) ˙⊂ M,
(M^{+}3)  a ˙∈ M ∧ f ∈ (M → M) → \begin{matrix}U(m (a, f)) ∧ a ˙∈ m (a, f) \\ ∧ f ∈ (m (a, f) → m (a, f)), \end{matrix}
(M^{+}4)  a ˙∈ M ∧ f ∈ (M → M) → m (a, f) ˙∈ M

We note some differences to the axioms of T_{0} + M^{+} given by Tupailo:

• In T_{0} + M^{+}, one has the limit operator u which gives (the name of) the next universe above a given name (see [Kah97]). Now, M is also closed under this operator: u : M → M. This is not necessary, since using m we can define easily for every universe a universe on top of it m(a, λx.x) (see also [JS02, Sect. 6]).

• Also, ℜ is closed under the limit operator u. Since universes are not closed under inductive generation, adding u most likely doesn’t add any strength to it. This is at least the case without the Mahlo universe: At the end of Sect. 4 in [JS02] as a consequence of a sophisticated model construction an outline of the argument is given, why adding closure under u to T_{0} doesn’t increase its proof-theoretic strength.

• T_{0} +M^{+} has no parameter a of m, so m only depends on f ˙∈(M → M). This doesn’t make any difference, since we can define for every a ˙∈ M and f ∈ (M → M) a g : M → M such that a universe is closed under g if and only if it is closed under f and a. (In Sect. 2 we showed how to encode a family of sets into a set such that a universe contains the code for the family if it contains the index and the elements of the family. We can do the same trick and encode two sets into one. Now let g x be the code for the two sets f x and a, and use the fact that universes are non-empty.)

• T_{0} + M^{+} doesn’t demand m (a, f) ˙⊂ M. In this respect, T_{0}(M)^{+} seems to be slightly stronger. However, any standard model used for determining an upper bound will fulfil this condition, and the well-ordering proof shouldn’t make use of it, therefore this condition should not add any proof theoretic strength to the theory. However, we believe that having this axiom is more aesthetically appealing, since m (a, f) should be a subuniverse of M.

For the extended predicative version of Mahlo, we formalize an internal Mahlo universe corresponding to T_{0}(M)^{+}.

5 Extended Predicative Mahlo

We aim to introduce new universes “from below”: given a “potential Mahlo universe”, i.e., a universe which should have the Mahlo property, we will enlarge this universe “carefully” by stages such that we get the desired property. The key difference between this approach compared to the axiomatic approach above is that we will not assume that f is a total function from names to names, but we will assume that it is total on the subuniverse which should be closed under f.

5.1 Relative f-Pre-Universe

For a given universe v—which is to be extended to a Mahlo universe—a name a and a given (arbitrary, possibly partial) function f we first define what it means that u is (the name of) a pre-universe, containing a, closed under f relative to v.

RPU(a, f, u, v) := (∀x.C(u, x) ∧ x ˙∈ v → x ˙∈ u) ∧  (1)
(a ˙∈ v → a ˙∈ u) ∧  (2)
(∀x ∈ u.f x ∈ v → f x ∈ u)  (3)

Thus, for given a, f, and v, a pre-universe u has the following properties:

• u is closed under the generators of EETJ, as long as the generated names are in v (1);

• if a is an element of v, it is an element of u (2);

• if f maps an element x of u to an element of v, then f x is in u; i.e., f x cannot be in v but outside u (3).

Fig. 1 illustrates a pre-universe. We see that a and f b are included in u, since they are in v. f c is not (yet) in v, so it is not included in u.

From a foundational point of view, this is a well-understood predicative inductive definition and we can introduce a straightforward induction principle to obtain least f-pre-universes. Using the new generator pre to name a pre-universe u, a least f-pre-universe pre (a, f, v) is characterized by the following axioms:

I. Least f-pre-universes

(EPM.1) ℜ_{ℜ}(v) → RPU(a, f, pre (a, f, v), v).

(EPM.2) ℜ_{ℜ}(v) ∧ RPU(a, f, φ, v) → ∀x ˙∈ pre (a, f, v).φ(x).

With (EPM.2) one gets immediately: ℜ_{ℜ}(v) → pre (a, f, v) ˙⊂ v.

c f c f b b  v a  u

Figure 1: A pre-universe

5.2 Independence

The f-pre-universes are defined relative to v; what we want is, of course, universes that no longer depend on v. Formally, we can express this independence by a formula Indep(a, f, u, v) which expresses that the “relativization to v” in the closure condition of RPU(a, f, u, v) is already fulfilled:

Indep(a, f, u, v) := (∀x.C(u, x) → x ∈ v) ∧
a ˙∈ v ∧
(∀x ˙∈ u.f x ˙∈ v)

Fig. 2 illustrates what it means for u to be independent of v, in case u = pre (a, f, v): a ˙∈ v and therefore a ˙∈ u; for a ˙∈ u we have f a ˙∈ v and therefore f a ˙∈ u, so u is closed under f. How f operates outside u does not really matter: it is possible that for some b ˙∈ v we have f b ˙∉ v.

The following lemma follows now directly from the definitions:

Lemma 1.

ℜ(u)∧ℜ_{ℜ}(v)∧RPU(a, f, u, v)∧Indep(a, f, u, v) → U(u)∧a ˙∈ u∧f ∈ (u → u).

Thus, under the condition Indep(a, f, pre (a, f, v), v), the least f-pre-universes pre (a, f, v) are actually universes. But the main property is that they are now independent of v in the sense that an enlargement of v will not change the extension of pre (a, f, v). This gives them, in fact, their predicative character. Formally this property is expressed in the following extended predicativity lemma.

fa  vIndep(a, f, u, v) b f b  u := pre (a, f, v)
Figure 2: Indep(a, f, u, v)

Lemma 2 (Extended Predicativity). In EETJ + (EPM.1) + (EPM.2) we can prove:

ℜ(v)∧ℜ_{ℜ}(w) ∧ Indep(a, f, pre (a, f, v), v) ∧ v ˙⊂ w → pre (a, f, v) ˙= pre (a, f, w).

As a corollary we get that an enlargement of v does not influence the independence property considered with respect to the bigger universe.

Corollary 3. In EETJ + (EPM.1) + (EPM.2) we can prove:

ℜ(v)∧ℜ_{ℜ}(w) ∧ Indep(a, f, pre (a, f, v), v) ∧ v ˙⊂ w → Indep(a, f, pre (a, f, w), w).

5.3 The Mahlo Universe

Intuitively, the idea to build the Mahlo universe is now to enlarge a potential Mahlo universe u and pre (a, f, u) in parallel up to the stage that pre (a, f, u) is independent of u (and, of course, doing this for all a and f). When the preuniverse is complete, it will not depend on any future additions to u.

Thus, axiomatically expressed, the Mahlo universe, named by M, has to be a universe, it has to be closed under inductive generation, and it has to collect, for every f, provided pre (a, f, M) is complete, an element representing pre (a, f, M) to it. Since in this case pre (a, f, M) is independent of M, we introduce a new name sub (a, f) which names the same type as pre (a, f, M), and add this element to M.

Fig. 3 illustrates the construction of M: If pre (a, f, M) is independent of M, it contains a and is closed under f; then the name sub (a, f) is added to

f  M sub (a, f) a b f b  pre (a, f, M) Indep(a, f, pre (a, f, M), M)

Figure 3: The extended predicative Mahlo universe

M (and the addition of sub (a, f) to M doesn’t affect the reason for originally adding it to M). Note again, that how f operates outside pre (a, f, M) does not really matter: it is possible that for some b ˙∈ M we have f b ˙∉ M, i.e., that M is not closed under f.

II. Mahlo universe

(EPM.3) U(M) ∧ i ∈ (M^{2} → M).

(EPM.4) Indep(a, f, pre (a, f, M), M) → sub (a, f) ˙∈ M ∧ sub (a, f) ˙= pre (a, f, M).

From (EPM.4) the theory will get its strength: Whenever we have a preuniverse pre (a, f, M), which is independent of M, we will have a name sub (a, f) of this universe in M. Note that by (EPM.1) pre (a, f, M) is already a pre-universe relative to M. Therefore, by Lemma 1 the premise of (EPM.4) implies that pre (a, f, M) is in fact a universe which is closed under a and f.

By Lemma 2 and Corollary 3 we know that independent universes do not depend on the universe used in the last parameter. Using the additional generator sub we can get rid of this redundant dependence in the name of the sub-universe with is actually added to M. More concretely, under the assumption Indep(a, f, pre (a, f, M), M) the addition of sub (a, f) to M does not affect the universe named by pre (a, f, M) (or sub (a, f)). “Philosophically spoken”, it does not affect the reason for its addition.

5.4 M is a Mahlo Universe

To show that M is indeed a Mahlo universe, we interpret T_{0}(M)^{+} into T_{0} + (EPM.1–4). This can be done translating m (a, f) by sub (a, f) and using the following lemma and theorem.

Lemma 4. ℜ(u) ∧ U(v) ∧ a ˙∈ v ∧ f ∈ (v → v) ∧ u ˙⊂ v ∧ RPU(a, f, u, v) → Indep(a, f, u, v) ∧ U(u) ∧ a ˙∈ u ∧ f ∈ (u → u)

Theorem 5. a ˙∈ M ∧ f ∈ (M → M) → sub (a, f) ˙∈ M ∧ sub (a, f) ˙⊂ M ∧ U(sub (a, f)) ∧ a ˙∈ sub (a, f) ∧ f ∈ (sub (a, f) → sub (a, f))

It is a straightforward exercise to formalise variants of (EPM.1–4) to capture an extended predicative internal Mahlo universe corresponding to T_{0}(M). These axioms might seem no more convincing than the axioms of axiomatic Mahlo, which just express that for every name a and function from names to names we can find a type closed under it. But these axioms are impredicative, since the collection of names has to have those closure princples. An extended predicative version of external Mahlo doesn’t have these problems, because the premise for introducing sub (a, f) doesn’t require f ∈ (ℜ → ℜ) which would refer to sub (a, f).

5.5 The Least Mahlo Universe

The addition of (EPM.1–4) to T_{0} yields already a theory of Mahloness with an appropriate proof-theoretic strength. However, the specific feature of the given approach is the possibility to axiomatize a least Mahlo universe.

For this we observe that, working in a set theoretical model of explicit mathematics, the extended predicative Mahlo universe can be defined as the least fixed point of the following operator

Γ(X) := {x | C(X, x)}∪{i (a, b) | a, b ∈ X}∪{sub (a, f) | Indep(a, f, pre(a, f, X), X)}

where Corollary 3 (adapted to the set theoretical setting) shows that Γ is monotone. The corresponding induction principle in set theory would be

Γ(A) ⊆ A → M ⊆ A

which means

(\begin{matrix}U(A) ∧ i ∈ (A^{2} → A) ∧ \\ (∀a, f.Indep(a, f, pre (a, f, A), A) → sub (a, f) ∈ A)) \end{matrix}

→ M ⊆ A

It doesn’t make sense to define pre (a, f, φ) for arbitrary formulas φ in Explicit Mathematics, and therefore we have to restrict the induction on M to “small sets”, i.e., elements of ℜ. We obtain the following

III. Induction for M (EPM.5) U(u) ∧ i ∈ (u^{2} → u) ∧

(∀f.∀a.Indep(a, f, pre (a, f, u), u) → sub (a, f) ˙∈ u)

→ M ˙⊂ u

Now, the theory EPM of extended predicative Mahlo can be defined as the extension of T_{0} by the axioms (EPM.1) – (EPM.5).

Note that such an induction principles as (EPM.5) cannot be formulated in the axiomatic approach, as the quantifier in the “induction step” has to range over arbitrary functions, not only those which are total from names to names. For the approach to Mahlo in Martin-Löf type theory, which is also based on total functions, the addition of an induction principle leads to a contradiction (see [Pal98, Theorem 6.1]), and this is probably also the case for axiomatic Mahlo in Explicit Mathematics. As, so far, there is no account for partial functions in Martin-Löf type theory which allows to refer to the collection of all terms, there is yet no possibility to define an extended predicative version of Mahlo. We note however that we don’t expect that the induction principles expressing minimality of M strengthen the theory. We expect the situation in this case to be similar to that in Martin-Löf type theory, where the second author has shown [Set97] that if one has a universe with certain closure conditions, one can define a set corresponding to the least universe having the same closure conditions—therefore having a least universe doesn’t add any strength.

6 Remarks on the Analysis of EPM

A proof-theoretic analysis of EPM will be given by the authors elsewhere. As we formalize an internal Mahlo universe, the strength of EPM is slightly above the one of KPM. One needs one extra recursively inaccessible above KPM, i.e., a model of EPM hast to be given in KPMI, KPω plus the existence of one recursively Mahlo ordinal M plus ∀x∃y.Ad(y) ∧ x ∈ y. For the lower bound one can use an embedding of the theory T_{0}(M)^{+} and then follow arguments of Tupailo [Tup03] to get a realization of an appropriate extension of CZF into T_{0}(M)^{+}. It seems to be feasible to get a lower bound by a wellordering proof for that extension of CZF. The argument above would show as well that the theory T_{0}(M)^{+} has the same strength as EPM and KPMI.

However, there are still a couple of questions concerning modifications of the theory. For instance, in [JKS01], a concept of name strictness is introduced. It expresses that generators only generate names for appropriate arguments (e.g., ℜ(co x) → ℜ(x)).^{5} In this context, also name induction is considered, which serves as an alternative to inductive generation or least universes to get a theory of the strength of T_{0}. The addition of name strictness and/or name induction may allow to simplify the definitions of relative f-pre-universe; however, there seems to be a subtle problem with formulating name strictness for generators of subuniverses of the Mahlo universe.

5This concept is analogous to—and motivated by—the usual strictness for definedness or strictness for the predicate N for natural numbers in applicative theories, cf. [Kah00].

Also, one may investigate the potential of the induction axioms, for both the subuniverses and the Mahlo universe itself, in concrete applications. As noted above, it is the specific feature of the extended predicative approach that it allows to formulate such induction axioms.

Finally, the formulation of an extended predicative Mahlo universe in a metapredicative setting (both with an external and an internal Mahlo universe) is still lacking. It should result, in principle, from the omission of inductive generation (and therefore (EPM.3)) and the induction axioms (EPM.2) and (EPM.5), and one probably needs to add ℜ_{ℜ}(v) → pre (a, f, v) ˙⊂ v, which is no longer provable without (EPM.2). These axioms allow an embedding of the metapredicative axiomatic external Mahlo universe (Theorem 5 holds with this modifications), which gives a lower bound for its proof theoretic strength. However one needs to carefully check whether any other adaptations of the axioms are needed, in order to avoid obtaining a theory which is stronger than the metapredicative axiomatic external Mahlo universe.

References

[Ara96a] Toshiyasu Arai. Proof theory of theories of ordinals I: Reflecting ordinals. Draft, 1996.

[Ara96b] Toshiyasu Arai. Systems of ordinal diagrams. Draft, 1996.

[Ara97a] Toshiyasu Arai. Proof theory of theories of ordinals II: Σ_{1} stability. Draft, 1997.

[Ara97b] Toshiyasu Arai. Proof theory of theories of ordinals III: Π_{1} collection. Draft, 1997.

[Ara00a] Toshiyasu Arai. Ordinal diagrams for Π_{3}-reflection. J. Symbolic Logic, 65(3):1375 – 1394, 2000.

[Ara00b] Toshiyasu Arai. Ordinal diagrams for recursively Mahlo universes. Arch. Math. Logic, 39(5):353 – 391, 2000.

[Ara03] Toshiyasu Arai. Proof theory for theories of ordinals. I. Recursively Mahlo ordinals. Ann. Pure Appl. Logic, 122(1 – 3):1 – 85, 2003.

[Ara04] Toshiyasu Arai. Proof theory for theories of ordinals. II. Π_{3}- reflection. Ann. Pure Appl. Logic, 129(1 – 3):39 – 92, 2004.

[Bac50] Heinz Bachmann. Die Normalfunktionen und das Problem der ausgezeichneten Folgen von Ordnungszahlen. Vierteljahresschrift der Naturforschenden Gesellschaft in Zürich, XCV:5–37, 1950.

[Bar75] Jon Barwise. Admissible Sets and Structures. An Approach to Definability Theory. Ω-series. Springer, 1975.

[Bee85] Michael Beeson. Foundations of Constructive Mathematics. Ergebnisse der Mathematik und ihrer Grenzgebiete; 3.Folge, Band 6. Springer, 1985.

[BF97] C. Burali-Forti. Una questione sui numeri transfiniti. Rendiconti del Circolo Matematico di Palermo (1884 - 1940), 11(1):154 – 164, December 1897. Translation in [Hei67], pp. 104 – 112.

[BFPS81] Wilfried Buchholz, Solomon Feferman, Wolfram Pohlers, and Wilfried Sieg. Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies, volume 897 of Lecture Notes in Mathematics. Springer, 1981.

[BS83] Wilfried Buchholz and Kurt Schütte. Ein Ordinazahlbezeichnungssystem für die beweistheoretische Abgrenzung der Π_{2}^{1}- Separation und Bar-Induktion. Sitzungsberichte der Bayerischen Akademie der Wissenschaften, Math.-Nat. Klasse, pages 99 – 132, 1983.

[BS88] Wilfried Buchholz and Kurt Schütte. Proof Theory of Impredicative Subsystems of Analysis. Bibliopolis, Naples, 1988.

[Buc92] Wilfried Buchholz. A simplified version of local predicativity. In P. Aczel, H. Simmons, and S. S. Wainer, editors, Proof Theory. A selection of papers from the Leeds Proof Theory Programme 1990, pages 115 – 147, Cambridge, 1992. Cambridge.

[DS03] Peter Dybjer and Anton Setzer. Induction-recursion and initial algebras. Annals of Pure and Applied Logic, 124:1 – 47, 2003.

[Fef64] Solomon Feferman. Systems of predicative analysis. Journal of Symbolic Logic, 29:1 – 30, 1964.

[Fef75] Solomon Feferman. A language and axioms for explicit mathematics. In J. Crossley, editor, Algebra and Logic, volume 450 of Lecture Notes in Mathematics, pages 87–139. Springer, 1975.

[Fef79] Solomon Feferman. Constructive theories of functions and classes. In M. Boffa, D. van Dalen, and K. McAloon, editors, Logic Colloquium 78, pages 159–224. North–Holland, Amsterdam, 1979.

[Fef05] Solomon Feferman. Predicativity. In S. Shapiro, editor, The Oxford Handbook of Philosophy of Mathematics and Logic, pages 590 – 624, Oxford, 2005. Oxford University Press.

[FJ96] Solomon Feferman and Gerhard Jäger. Systems of explicit mathematics with non-constructive μ-operator. Part II. Annals of Pure and Applied Logic, 79(1):37–52, 1996.

[Gen36] Gerhard Gentzen. Die Widerspruchsfreiheit der reinen Zahlentheorie. Mathematische Annalen, 112:493 – 565, 1936.

[GR94] Edward Griffor and Michael Rathjen. The strength of some Martin-Löf type theories. Archive for Mathematical Logic, 33(5):347, 1994.

[Hau08] Feliz Hausdorff. Grundzüge einer Theorie der geordneten Mengen. Mathematische Annalen, 65(4):435 – 505, 1908.

[Hei67] Jean van Heijenoort. From Frege to Gödel. Harward University Press, 1967.

[Hei86] G. Heinzmann. Poincaré, Russell, Zermelo et Peano. Textes de la discussion (1906 – 1912) sur les fondements des mathématiques: des antinomies á la preédicativité. Albert Blanchard, Paris, 1986.

[Hin78] P.G. Hinman. Recursion-Theoretic Hierarchies. Springer, 1978.

[How72] W. A. Howard. A system of abstract constructive ordinals. J. Symbolic Logic, 37:355 – 374, 1972.

[Jäg79] Gerhard Jäger. Die konstruktible Hierarchie als Hilfsmittel zur beweistheoretischen Untersuchung von Teilsystemen der Analysis. PhD thesis, Universität München, 1979. Dissertation.

[Jäg80] Gerhard Jäger. Theories for iterated jumps. Handwritten Notes, 1980.

[Jäg83] Gerhard Jäger. A well-ordering proof for Feferman’s theory T_{0}. Archiv f. Math. Logik und Grundlagenforschung, 23:65 – 77, 1983.

[Jäg01] Gerhard Jäger. First order theories for nonmonotonic inductive definitions: Recursively inaccessible and Mahlo. Journal of Symbolic Logic, 66(3):1073–1089, September 2001.

[Jäg05] Gerhard Jäger. Metapredicative and explicit Mahlo: a prooftheoretic perspective. In René Cori, Alexander Razborov, Stevo Todorčević, and Carol Wood, editors, Logic Colloquium 2000, Lecture Notes in Logic, pages 272 – 293. A K Peters. Association for Symbolic Logic, 2005.

[JKS99] Gerhard Jäger, Reinhard Kahle, and Thomas Strahm. On applicative theories. In A. Cantini, E. Casari, and P. Minari, editors, Logic and Foundation of Mathematics, pages 83–92. Kluwer, 1999.

[JKS01] Gerhard Jäger, Reinhard Kahle, and Thomas Studer. Universes in explicit mathematics. Annals of Pure and Applied Logic, 109(3):141–162, 2001.

[JKSS99] Gerhard Jäger, Reinhard Kahle, Anton Setzer, and Thomas Strahm. The proof-theoretic analysis of transfinitely iterated fixed point theories. Journal of Symbolic Logic, 64(1):53 – 67, 1999.

[JP82] Gerhard Jäger and Wolfram Pohlers. Eine beweistheoretische Untersuchung von (Δ_{2}^{1} − CA) + BI und verwandter Systeme. Sitzungsberichte der Bayer. Akad. d. Wiss., Math.-Nat. Kl., pages 1 – 28, 1982.

[JS01] Gerhard Jäger and Thomas Strahm. Upper bounds for metapredicative Mahlo in explicit mathematics and admissible set theory. Journal of Symbolic Logic, 66(2):935–958, 2001.

[JS02] Gerhard Jäger and Thomas Studer. Extending the system t_{0} of explicit mathematics: the limit and mahlo axioms. Annals of Pure and Applied Logic, 114(1–3):79–101, 2002.

[JS05] Gerhard Jäger and Thomas Strahm. Reflections on reflections in explicit mathematics. Annals of Pure and Applied Logic, 136(1– 2):116–133, 2005.

[Kah97] Reinhard Kahle. Uniform limit in explicit mathematics with universes. Technical Report IAM-97-002, IAM, Universität Bern, 1997.

[Kah00] Reinhard Kahle. N-strictness in applicative theories. Archive for Mathematical Logic, 39(2):125 – 144, February 2000.

[Kah07] Reinhard Kahle. The applicative realm, volume 40 of Textos de Matemática. Departamento de Matemática, Universidade de Coimbra, 2007. Habilitationsschrift, Fakultät für Informationsund Kommunikationswissenschaften, Universität Tübingen.

[Kre60] Georg Kreisel. Ordinal logics and the characterization of informal concepts of proof. In John A. Todd, editor, Proceedings of the International Congress of Mathematicians, 14 – 21 Aug 1958, pages 289 – 299, Cambridge, 1960. Cambridge University Press.

[Kri64] S. Kripke. Transfinite recursion on admissible ordinals, I, II (abstracts). J. Symbolic Logic, 29:161 – 162, 1964.

[Lei94] Daniel Leivant. Ramified recurrence and computational complexity i: Word recurrence and poly-time. In Peter Clote and Jeffrey Remmel, editors, Feasible Mathematics II, pages 320 – 343, New York, 1994. Birkhäuser-Boston.

[Lei95] Daniel Leivant. Intrinsic theories and computational complexity. In Daniel Leivant, editor, Logic and Computational Complexity, pages 177 – 194. Springer Lecture Notes in Computer Science 960, 1995.

[Mah11] Paul Mahlo. Über linear transfinite Mengen. Berichte über die Verhandlungen der Königlich Sächsischen Gesellschaft der Wissenschaften zu Leipzig. Mathematisch-Physische Klasse, 63:187 – 225, 1911.

[Mah12] Paul Mahlo. Zur Theorie und Anwendung der ϱ_{0}-Zahlen. Berichte über die Verhandlungen der Königlich Sächsischen Gesellschaft der Wissenschaften zu Leipzig. Mathematisch-Physische Klasse, 64:108 – 112, 1912.

[Nel86] E. Nelson. Predicative Arithmetic. Princeton University Press, Princeton, 1986.

[Pal98] E. Palmgren. On universes in type theory. In G. Sambin and J. Smith, editors, Twenty five years of constructive type theory, pages 191 – 204, Oxford, 1998. Oxford University Press.

[Par92] Charles Parsons. Impredicativity of induction. In Michael Detlefsen, editor, Proof, Logic and formalization, pages 139 – 161. Routledge, 1992.

[Pla66] R. Platek. Foundations of recursion theory. PhD thesis, Stanford University, Standford, California, 1966. Contains Supplement.

[Poh96] Wolfram Pohlers. Pure proof theory. Bulletin of Symbolic Logic, 2(2):159–188, 1996.

[Poh98] Wolfram Pohlers. Subsystems of set theory and second order number theory. In S. Buss, editor, Handbook of Proof Theory, chapter IV, pages 209–335. North-Holland, 1998.

[Poi06] H. Poincaré. Les mathématiques et la logique. Revue de métaphysique et de morale, 14:294 – 317, 1906. Reprinted in [Hei86], 11 – 53.

[Rat90] Michael Rathjen. Ordinal notations based on a weakly Mahlo cardinal. Arch. Math. Log., 29:249 – 263, 1990.

[Rat91] Michael Rathjen. Proof-theoretical analysis of KPM. Arch. Math. Log., 30:377 – 403, 1991.

[Rat92] Michael Rathjen. Eine Ordinalzahlanalyse der Π_{3}–Reflexion. Habilitationsschrift, Westfälische Wilhelms–Universität Münster, 1992.

[Rat94a] Michael Rathjen. Collapsing functions based on recursively large cardinals: A well-ordering proof for KPM. Archive for Mathematical Logic, 33:35–55, 1994.

[Rat94b] Michael Rathjen. Proof theory of reflection. Ann. Pure Appl. Logic, 68:181 – 224, 1994.

[Rat95] Michael Rathjen. Recent advances in ordinal analysis: Π_{2}^{1}-CA and related systems. Bulletin of Symbolic Logic, 1:468 – 485, 1995.

[Rat96] Michael Rathjen. The recursively Mahlo property in second order arithmetic. Mathematical Logic Quarterly, 42:59–66, 1996.

[Rat05a] Michael Rathjen. An ordinal analysis of parameter free Π_{2}^{1}- comprehension. Arch. Math. Log., 44(3):263 – 362, April 2005.

[Rat05b] Michael Rathjen. An ordinal analysis of stability. Arch. Math. Logic, 44(1):1 – 62, January 2005.

[Ric71] Wayne Richter. Recursively Mahlo ordinals and inductive definitions. In R. O. Gandy and C. E. M. Yates, editors, Logic Colloquium ’69, pages 273–288. North-Holland, 1971.

[Rus02] Bertrand Russell. Letter to Frege. Published in [Hei67], pp. 124 – 125, 1902.

[Rus06] Bertrand Russell. On some difficulties in the theory of transfinite numbers and order types. Proc. London Mathematical Society, 4:29 –53, 1906. Reprinted in [Rus73], pp. 135 – 164.

[Rus73] Bertrand Russell. Essays in Analysis. George Braziller, New York, 1973. Edited by D. Lackey.

[Sch65a] Kurt Schütte. Einge Grenze für die Beweisbarkeit der Transfiniten Induktion in der verzweigten Typenlogik. Archiv für Mathematische Logik und Grundlagenforschung, 7:45 – 60, 1965.

[Sch65b] Kurt Schütte. Predicative well-orderings. In J. Crossley and M. Dummett, editors, Formal Systems and recursive functions. Proc. of the 8th Logic Colloquium Oxford 1963, pages 280 – 303, Amsterdam, 1965. North Holland.

[Sch77] Kurt Schütte. Proof Theory. Springer, 1977.

[Set97] Anton Setzer. Defining the least universe in Martin-Löf’s type theory. Bulletin of Symbolic Logic, 3:276 – 277, 1997.

[Set98] Anton Setzer. Well-ordering proofs for Martin-Löf type theory. Annals of Pure and Applied Logic, 92:113 – 159, 1998.

[Set00] Anton Setzer. Extending Martin-Löf type theory by one Mahlouniverse. Archive for Mathematical Logic, 39:155–181, 2000.

[Sim99] Stephen G. Simpson. Subsystems of second-order arithmetic. Springer, 1999.

[Str99] Thomas Strahm. First steps into metapredicativity in explicit mathematics. In S. B. Cooper and J. Truss, editors, Sets and Proofs, pages 383 – 402, Cambridge, 1999. Cambridge University Press.

[Str02] Thomas Strahm. Wellordering proofs for metapredicative Mahlo. Journal of Symbolic Logic, 67(1):260–278, 2002.

[Tak87] G. Takeuti. Proof Theory. North–Holland Publishing Company, Amsterdam, second edition, 1987.

[Tup03] Sergei Tupailo. Realization of constructive set theory into explicit mathematics: a lower bound for impredicative Mahlo universe. Annals of Pure and Applied Logic, 120(1-3):165 – 196, 2003.

[TvD88] Anne Troelstra and Dirk van Dalen. Constructivism in Mathematics, vol II. North Holland, 1988.

[Wey18] Hermann Weyl. Das Kontinuum. Kritische Untersuchungen über die Grundlagen der Analysis. Veit, Leipzig, 1918.