Applications of Large Cardinals to Constructive Set Theory

The main aim of this project is to study the structure of the mathematical universe under variants of the standard axioms of ZFC (Zermelo-Fraenkel set theory with choice). In particular, how different the universe behaves under ZF on the one hand and the intuitionistic set theories IZF (Intuitionistic Zermelo-Fraenkel set theory) and CZF (Constructive Zermelo-Fraenkel set theory) on the other hand. In order to do this, the work will be split into two parts. The first is to explore the nature of large cardinal axioms in the classical setting without choice and how much the equivalences between certain definitions of large cardinals in ZFC break down when choice is dropped. The second, which concerns intuitionistic theories, will involve studying the notion of large sets. These are sets with properties analogous to the initial segment of the von Neumann hierarchy up to a large cardinal.
One of the many problems one encounters when working in a theory without choice is the difficulty in producing models of these theory. For example, assuming that there is a model of ZFC, the Lowenheim-Skolem Theorem gives a model of any cardinality. However it is known that that the statement ``Every infinite model in a language of cardinality K has an elementary submodel of cardinality K" is equivalent to choice of length K. Therefore, when working with weak choice or no choice at all, it can be difficult to produce ``small" models. Another result where we don't know whether choice is needed or not is the proof that in ZFC there is no non-trivial elementary embedding of the universe into itself.
Large sets in the intuitionistic context were first formally introduced in 1984 in a paper by H. Friedman and A. Scedrov. The purpose of this paper was to introduce the notions of inaccessible sets, Mahlo sets and sets that were the critical point of an elementary embedding of the universe into some transitive class model $M$ of IZF. The authors then go on to show that IZF plus the existence of some large set is equiconsistent to its classical counterpart. A more substantial study of large cardinals has been undertaken by P. Aczel and M. Rathjen and is contained within their draft of a book on Constructive Set Theory. This work is introduces the idea of a regular set which is an integral part of the definition of an inaccessible set. While both intuitionistic theories, inaccessible sets in CZF and fundamentally different from those in IZF. This is because, while in IZF the authors just wanted sets that were models of IZF (so were in fact closer to the definition of wordly cardinals), within CZF the authors wanted a set that had precisely those properties of in the classical case for inaccessible cardinals. The constructive formulation also allows for a second definition of what it means for a set to be inaccessible, giving a simple criterion of properties that the set must satisfy rather than solely asserting that the set satisfies every axiom of the theory.
The most in depth discussion of large sets in a constructive setting is given in Albert Ziegler's thesis, ``Sets in Constructive Set Theory". This work gives a rigorous formulation of constructive variants of many of the lower axioms in the large cardinal hierarchy. This culminates in an extensive review of two important aspects of the study of large sets; realisability and elementary embeddings. In particular, the results from this thesis show how differently large sets behave from their classical counterparts. Also, unlike in the classical case, the assumption that there are more large sets satisfying some property does not necessarily increasing the consistency strength of the theory. E.g., if it is consistent that there is one inaccessible then it is consistent that there are a proper class of them. Some of the many questions which will occupy the research for the thesisover the coming years are:
1. How do large cardinals differ without choice. E.g. what happens to the many equivalent formu