Higher-order conceptual mathematics and intuitionistic set theory: Well-orderings, ordinals and Gödel’s L

This thesis studies the construction of realisability models from various partial combinatory algebras in formal theories of both arithmetic and set theory. The focus is on the representation of ‘set objects’ (or higher-order objects, respectively) and the implementation of transfinite recursion along well-orderings and set-theoretic ordinals for the purpose of interpreting specific axioms.

For the arithmetic part, we study a semi-intuitionistic theory of third-order conceptual mathematics, CM, proposed by Nik Weaver. We provide an ordinal analysis through a realisability interpretation in fragments of classical second-order arithmetic and use it to gauge the effect of adding different instances of the transfinite induction scheme on a global well-ordering to the proof-theoretic strength of the system.

The rest of the thesis then implements several realisability arguments over different partial combinatory algebras for constructive Zermelo–Fraenkel set theory. We obtain multiple consistency and independence results surrounding the intuitionistic ordinals and Gödel’s constructible universe L in this way. We also analyse and resolve the open problem of whether adding the axiom V = L will increase the consistency strength of certain constructive set theories, giving a negative answer.

The set-theoretic contribution of this thesis is the method of incomparable codings, which utilises the existence of incomparable ordinals in intuitionistic set theory to encode information about arbitrary sets into a single ordinal. In conjunction with Paul Taylor’s notion of plump ordinals, this leads to a very useful mechanism for verifying exotic properties of L in intuitionistic models.