Theory of proveit.logic.sets.comprehension¶
Subset comprehension is a way to define a subset of a set by listing properties/conditions of the elements of the subset. For example, $\{x~|~Q(x)\}_{x \in S}$, is the subset of $S$ for which every element $x$ satisfies the condition $Q(x)$.
More generally, comprehension may define a set by mapping subset elements via some function. For example, $\{f(x)~|~Q(x)\}_{x \in S}$ is the set that contains only and all $f(x)$ elements such that $x \in S$ and $Q(x)$ is TRUE. This furthermore generalizes to mapping any number of elements and specifying any number of conditions. For example, $\{f(x, y)~|~Q(x, y), R(x, y)\}_{x, y \in S}$ is the set that contains only and all of $f(x, y)$ elements such that $x \in S$, $y \in S$, $Q(x, y)$, and $R(x, y)$. It is also possible not to specify any conditions and simply define a direct map of a set: $\{f(x)\}_{x \in S}$ or $\{f(x, y)\}_{x, y \in S}$.
To avoid Russell's paradox (the set of all sets which, paradoxically, do not contain themselves), axioms should only define sets that preserve the property of having a well-defined, ordinal rank and therefore set membership is always irreflexive (a set cannot contain itself). Set rank is essentially the depth of the tree of set membership relations (e.g., the empty set has rank 0, a set containing only empty sets is rank 1, etc.). By our convention in the proveit.logic.sets theory package, if something contains an element via set membership (InSet), it is a defacto set and should have a well-define ordinal rank. Anything that contains no elements, or is consistent with containing no elements, may be regarded as having rank 0 just like the emtpy set. For example, proper classes have rank 0 (these can contain members via class membership but not set membership).
As an obvious corollary, no universal set should be defined via axioms.
import proveit
%theory
