6
$\begingroup$

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?

Improve this question
$\endgroup$

1 Answer 1

Reset to default
4
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • 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
    Commented Jan 11, 2010 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
    Commented Jan 11, 2010 at 18:56

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .