nLab dependently sorted set theory

Idea

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 $a \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

• unsorted set theory
• two-sorted set theory
• dependently sorted set theory
• material set theory
• structural set theory
• structurally presented set theory
• set-level type theory