In [1]:

```
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
```

**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.**

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

In [2]:

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

In [3]:

```
%end axioms
```