Church's simple type theory is known to be equiconsistent to a bounded version of Zermelo's set theory (using only bounded quantifiers).

Is there also a type theoretical formulation of mathematical foundations which is equiconsistent to some unbounded set theory based on Zermelo's work?

  • 2
    $\begingroup$ Rathjen showed in his Constructive Zermelo-Fraenkel Set Theory, Power Set, and the Calculus of Constructions that there is a type theory (namely $\mathbf{MLV_P}$) whose proof-theoretic strength exceeds that of Zermelo set theory. $\endgroup$
    – Hanul Jeon
    Jan 5, 2020 at 16:33

1 Answer 1


Yes, there is a type theory equiconsistent with unbounded Zermelo set theory. In the paper λZ: Zermelo's Set Theory as a PTS with 4 Sorts Alexandre Miquel presents a type theory $\mathrm{\lambda Z}$ that is shown equiconsitent to the Zermelo Set Theory $\mathrm{Z}$. This type theory $\mathrm{\lambda Z}$ is a subsystem of System $F\omega$ with universes.

The equiconsistency is shown by embedding $\mathrm{IZ} + \mathrm{AFA} + \mathrm{TC}$ (Intuinonistic Zermelo with Aczel's antifoundation axiom and the existance of transitive closures) into $\mathrm{\lambda Z}$ by representing sets as pointed graphs. This theory $\mathrm{IZ} + \mathrm{AFA} + \mathrm{TC}$ is itself equiconsistent to $\mathrm{Z}$.


You must log in to answer this question.

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