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

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, Not, Equals, InSet, in_bool, NotInSet, EmptySet
from proveit.numbers import Exp, Natural, one
from proveit import x, S, f, i, n
from proveit.logic.sets import each_x_in_S
%begin axioms

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

Set membership should be either true or false (though one might not know which it is), and thus we might naively expect to include here an axiom for set membership being in the Boolean set, something like

$\text{membership_in_bool} = \forall_{x, S}\;(x\in S) \in Boolean$

This would be problematic, however, and open up the system to Russell's paradox. Instead we use whether or not membership can be proven to be in the Boolean set to dictate whether something is a set or not.

Define an exponentiated set.

Bob has a good suggestion to move this to a new theory, proveit.logic.sets.cartesian_product, as a theorem. The axioms would define S^n = S x S x ... S and the axiom would be a more general one about membership in a general cartesian product.

exp_set_def = Forall(n, Forall((x, S), Equals(InSet(x, Exp(S, n)), And(Equals(Len(x), n), each_x_in_S))), domain=Natural)

$x \notin S$ is defined as the negation of $x \in S$ for all $x$ and $S$:

not_in_set_def = Forall((x, S), Equals(NotInSet(x, S), Not(InSet(x, S))))

not_in_set_def:

%end axioms

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