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


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.