first-order set theory in nLab

+-- {: .rightHandSide}
+-- {: .toc .clickDown tabindex="0"}
### Context
#### Foundations
+-- {: .hide}
[[!include foundations - contents]]
=--
=--
=--

# Contents
* table of contents
{:toc}

## 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. 

## Related concepts

* [[predicate logic]]

* [[set-level type theory]]

## References

* [[Steve Awodey]], [[Carsten Butz]], [[Alex Simpson]], [[Thomas Streicher]], *Relating first-order set theories, toposes and categories of classes*, Annals of Pure and Applied Logic **165** 2 (2014) 428-502 &lbrack;[doi:10.1016/j.apal.2013.06.004](https://doi.org/10.1016/j.apal.2013.06.004)&rbrack;

[[!redirects first-order set theories]]