Type-Two Well-Ordering Principles, Admissible Sets, and Pi^1_1-Comprehension

This thesis introduces a well-ordering principle of type two, which we call the Bachmann-Howard principle. The main result states that the Bachmann-Howard principle is equivalent to the existence of admissible sets and thus to Pi^1_1-comprehension. This solves a conjecture of Rathjen and Montalbán. The equivalence is interesting because it relates "concrete" notions from ordinal analysis to "abstract" notions from reverse mathematics and set theory. A type-one well-ordering principle is a map T which transforms each well-order X into another well-order T[X]. If T is particularly uniform then it is called a dilator (due to Girard). Our Bachmann-Howard principle transforms each dilator T into a well-order BH(T). The latter is a certain kind of fixed-point: It comes with an "almost" monotone collapse theta:T[BH(T)]->BH(T) (we cannot expect full monotonicity, since the order-type of T[X] may always exceed the order-type of X). The Bachmann-Howard principle asserts that such a collapsing structure exists. In fact we define three variants of this principle: They are equivalent but differ in the sense in which the order BH(T) is "computed". On a technical level, our investigation involves the following achievements: a detailed discussion of primitive recursive set theory as a basis for set-theoretic reverse mathematics; a formalization of dilators in weak set theories and second-order arithmetic; a functorial version of the constructible hierarchy; an approach to deduction chains (Schütte) and beta-completeness (Girard) in a set-theoretic context; and a beta-consistency proof for Kripke-Platek set theory. Independently of the Bachmann-Howard principle, the thesis contains a series of results connected to slow consistency (introduced by S.-D. Friedman, Rathjen and Weiermann): We present a slow reflection statement and investigate its consistency strength, as well as its computational properties. Exploiting the latter, we show that instances of the Paris-Harrington principle can only have extremely long proofs in certain fragments of arithmetic.