nLab first-order set theory

Contents

Context

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axiom

Removing axioms

Contents

Idea

A first-order set theory is a set theory which is a first-order theory. These include unsorted set theories like ZFC and fully formal ETCS, simply sorted set theories like the two-sorted presentation of ETCS, and dependently sorted set theories like the usual presentation of ETCS and SEAR.

It contrasts with other approaches to set theory which are not first-order theories, such as set-level type theories like XTT or Martin-Löf type theory with a type of all propositions and UIP/axiom K, all of which could be considered to be set theories.

References

Last revised on December 3, 2022 at 06:20:51. See the history of this page for a list of all contributions to it.