Axioms for the theory of proveit.logic.sets.comprehension

import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit.logic import Forall, And, Equals, InSet, SetOfAll, Exists
from proveit import n, x, Q, f, Qy
from proveit.core_expr_types import y_1_to_n, f__y_1_to_n, Q__y_1_to_n, S_1_to_n
from proveit.logic.sets import general_comprehension_fyn
from proveit.numbers import Exp, Natural, NaturalPos
%begin axioms

Defining axioms for theory 'proveit.logic.sets.comprehension'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

Define general set comprehension any mapping $y \mapsto f(y)$ applied to the set of elements $y$ of $S$ such that $Q(y)$: TODO: CHANGE THIS TO A DEFINITION USING UnionOfAll: {f(x) | Q(x)}{x in S} = Union{x in S | Q(x)} {f(x)}

comprehension_def = Forall(n, 
                           Forall((S_1_to_n, Q, f, x), 
                                  Equals(InSet(x, general_comprehension_fyn),
                                         Exists(y_1_to_n, Equals(x, f__y_1_to_n), 
                                                domains=[S_1_to_n], conditions=[Q__y_1_to_n]))\
                                  .with_wrap_before_operator()),
                          domain=NaturalPos)

comprehension_def:

NOTE: Comprehension defines a subset of some set $S$, and a "universal" set must not be allowed. Otherwise you could define Russell's set, $R = \{x~|~x \notin x\}_x$, which results in paradox upon asking whether or not $R \in R$ (if it is, then it cannot be; if it is not, then it must be). But if $x \in S$ can only be true if $S$ is a "properly" defined set which cannot contain itself, then Russell's paradox is avoided. Note that, although using the same notation in formatting, set membership is distinct from class membership, and we cannot apply subset comprehension to proper classes.

%end axioms

These axioms may now be imported from the theory package: proveit.logic.sets.comprehension