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. (shrink)

The aim of this paper is the analysis of uniformity in Feferman's explicit mathematics. The proof-strength of those systems for constructive mathematics is determined by reductions to subsystems of second-order arithmetic: If uniformity is absent, the method of standard structures yields that the strength of the join axiom collapses. Systems with uniformity and join are treated via cut elimination and asymmetrical interpretations in standard structures.