Palmgren (1997), On universes in type theory, discusses work of several theorists that provide what we might call a family of Large Universe Axioms (LUAs) for predicative type theory, culminating in Rathjen's MLF_w that corresponds to Kripke-Platek set theory with a weakened epsilon-induction principle. He also provides a criterion for recognising predicative universe-forming operations: does it come equipped with an induction rule?

That work and work since has been suggestive of a partial analogy between LCAs in set theory (specifically KP set theory) and LUAs in type theory. This is provocative and interesting, but what I have read has left me unclear about how productive the analogy is. How well-founded is the analogy? What are its limits?


The analogy between universes in type theory and the Mahlo hierarchy in set theory has been analyzed in many different ways by Michael Rathjen. (This builds on his analysis of KPM, but ML type theories with universes came in later in the game.)

I don't have the Palmgren paper you refer to, but I think the following paper is closely related to your questions:

Rathjen, Griffor, Palmgren, Inaccessibility in constructive set theory and type theory, Ann. Pure Appl. Logic 94 (1998), 181-200.

This is not the only way of relating universes in type theory and inaccessibles in set theory, another one is presented by Anton Setzer in Extending Martin-Löf type theory by one Mahlo-universe and further investigated by Rathjen in Realizing Mahlo set theory in type theory.

  • 1
    $\begingroup$ Thanks. Palmgren kicked off the field with his PhD, which described the kind of constructions on universes need to make LUAs. IIRC, Setzer distinguishes between strong and weak Mahlo universes, where only the weak construction gives an induction principle. $\endgroup$ – Charles Stewart Jan 11 '10 at 13:57
  • $\begingroup$ I should have made it clearer which part of your question I was addressing. I conveniently ignored the induction part of your question, and I really don't know what happens there. Thanks for pointing out the issue in Setzer's work. I don't remember such issues in RGP, but the context is very different. $\endgroup$ – François G. Dorais Jan 11 '10 at 18:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.