basic constructions:
strong axioms
further
Simply sorted set theory is a set theory which is a first order theory without dependent sorts; i.e. written in first order logic and whose domains of discourse (called sorts here) do not on other domains of discourse. In addition, membership $a \in A$ is a relation, rather than a judgment as in dependently sorted set theory. Simply sorted set theories come in both material set theories and structural set theories.
Simply sorted set theory could be distinguished between how many sorts the theory has; these include
A notion of set and element in a simply sorted first-order theory consists of:
A sort $S$ of probable sets. By probable set, we mean that certain terms of $S$ are to be considered as the sets in the theory.
A sort $E$ of probable elements. By probable element, we mean that certain terms of $E$ are to be considered as the elements in the theory.
A binary predicate in $S$, $(-)=_S(-)$, called definitional equality of sets
A binary predicate in $E$, $(-)=_E(-)$, called equality of elements
A unary predicate in $S$, $\mathrm{set}(-)$, called being a set
A unary predicate in $E$, $\mathrm{element}(-)$, called being an element
A binary predicate in $E$ on the left and $S$ on the right, $(-)\in(-)$, called membership
such that
$(-)=_E(-)$ is an equivalence relation
if $a \in b$, then $a$ is an element and $b$ is a set
In one-sorted set theory, the sorts $E$ and $S$ are the same sort.
Last revised on November 19, 2022 at 20:38:17. See the history of this page for a list of all contributions to it.