nLab dependently sorted set theory




The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms



Dependently sorted set theory is a set theory which is a first order theory with dependent sorts; i.e. written in first order logic and whose domains of discourse (called sorts here) depend on other domains of discourse. In addition, membership aAa \in A is a judgment, rather than a proposition as in simply sorted set theory. By and large, dependently sorted set theories are structural set theories, and are structurally presented set theories.

Examples of dependently sorted set theories include the usual presentations of ETCS and SEAR.

Dependently sorted set theory is different from set-level intensional type theories. Intensional type theories satisfy the propositions as some types principle, where every proposition is a set and the first order logic is built out of the type theory itself. On the other hand, dependently sorted set theories are first order logic over dependent type theory and keep sets and propositions separate.

See also

Last revised on November 17, 2022 at 14:58:37. See the history of this page for a list of all contributions to it.