# Type theoretical foundation of unbounded Zermelo set theory

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?

• 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. Jan 5 '20 at 16:33

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}$$.