Induction–recursion is a powerful definition method in intuitionistic type theory. It extends inductive definitions and allows us to define all standard sets of Martin-Löf type theory as well as a large collection of commonly occurring inductive data structures. It also includes a variety of universes which are constructive analogues of inaccessibles and other large cardinals below the first Mahlo cardinal. In this article we give a new compact formalization of inductive–recursive definitions by modeling them as initial algebras in slice categories. (...) We give generic formation, introduction, elimination, and equality rules generalizing the usual rules of type theory. Moreover, we prove that the elimination and equality rules are equivalent to the principle of the existence of initial algebras for certain endofunctors. We also show the equivalence of the current formulation with the formulation of induction–recursion as a reflection principle given in Dybjer and Setzer 93). Finally, we discuss two type-theoretic analogues of Mahlo cardinals in set theory: an external Mahlo universe which is defined by induction–recursion and captured by our formalization, and an internal Mahlo universe, which goes beyond induction–recursion. We show that the external Mahlo universe, and therefore also the theory of inductive–recursive definitions, have proof-theoretical strength of at least Rathjen's theory KPM. (shrink)

In this paper we discuss extensions of Feferman's theory T 0 for explicit mathematics by the so-called limit and Mahlo axioms and present a novel approach to constructing natural recursion-theoretic models for systems of explicit mathematics which is based on nonmonotone inductive definitions.

The goals of reduction andreductionism in the natural sciences are mainly explanatoryin character, while those inmathematics are primarily foundational.In contrast to global reductionistprograms which aim to reduce all ofmathematics to one supposedly ``universal'' system or foundational scheme, reductive proof theory pursues local reductions of one formal system to another which is more justified in some sense. In this direction, two specific rationales have been proposed as aims for reductive proof theory, the constructive consistency-proof rationale and the foundational reduction rationale. However, (...) recent advances in proof theory force one to consider the viability of these rationales. Despite the genuine problems of foundational significance raised by that work, the paper concludes with a defense of reductive proof theory at a minimum as one of the principal means to lay out what rests on what in mathematics. In an extensive appendix to the paper,various reduction relations betweensystems are explained and compared, and arguments against proof-theoretic reduction as a ``good'' reducibilityrelation are taken up and rebutted. (shrink)

In this article we introduce systems for metapredicative Mahlo in explicit mathematics and admissible set theory. The exact upper proof-theoretic bounds of these systems are established.

We give an overview of recent results in ordinal analysis. Therefore, we discuss the different frameworks used in mathematical proof-theory, namely "subsystem of analysis" including "reverse mathematics", "Kripke-Platek set theory", "explicit mathematics", "theories of inductive definitions", "constructive set theory", and "Martin-Löf's type theory".

We present well-ordering proofs for Martin-Löf's type theory with W-type and one universe. These proofs, together with an embedding of the type theory in a set theoretical system as carried out in Setzer show that the proof theoretical strength of the type theory is precisely ψΩ1Ω1 + ω, which is slightly more than the strength of Feferman's theory T0, classical set theory KPI and the subsystem of analysis + . The strength of intensional and extensional version, of the version à (...) la Tarski and à la Russell are shown to be the same. (shrink)

We define a realizability interpretation of Aczel's Constructive Set Theory CZF into Explicit Mathematics. The final results are that CZF extended by Mahlo principles is realizable in corresponding extensions of T 0 , thus providing relative lower bounds for the proof-theoretic strength of the latter.

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)

We give a broad discussion of reflection principles in explicit mathematics, thereby addressing various kinds of universe existence principles. The proof-theoretic strength of the relevant systems of explicit mathematics is couched in terms of suitable extensions of Kripke–Platek set theory.