In the early 1980s, the forum of ordinal analysis switched from analysing subsystems of second order arithmetic and theories of inductive definitions to set theories. The new results were much more uniform and elegant than their predecessors. This thesis uses techniques for the ordinal analysis of set theories developed over the past 30 years to extract some useful information about Kripke Platek set theory, KP and some related theories.
First I give a classification of the provably total set functions of KP, this result is reminiscent of a classic theorem of ordinal analysis, characterising the provably total recursive functions of Peano Arithmetic, PA.
For the remainder of the thesis the focus switches to intuitionistic theories. Firstly, a detailed rendering of the ordinal analysis of intuitionistic Kripke-Platek set theory, IKP, is given. This is done in such a way as to demonstrate that IKP has the existence property for its verifiable ⌃ sentences. Combined with the results of [40] this has important implications for constructive set theory.
It was shown in [42] that sometimes the tools of ordinal analysis can be applied in the context of strong set-theoretic axioms such as power set to obtain a characterisation of a theory in terms of provable heights of the cumulative hierarchy. In the final two chapters this machinery is applied to ‘scale up’ the earlier result about IKP to two stronger theories IKP(P) and IKP(E). In the case of IKP(E) this required considerable new technical legwork. These results also have important applications within constructive set theory.
