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 Equals, Not, Implies, Forall, TRUE, FALSE, Boolean, in_bool
from proveit import A
%begin axioms
```

**Implicit in the following set of axioms is that $\lnot A$ is in Boolean iff
$A$ is in Boolean. Otherwise, $\lnot A$ is simply undefined.**

In [2]:

```
not_t = Equals(Not(TRUE), FALSE)
```

Out[2]:

In [3]:

```
not_f = Equals(Not(FALSE), TRUE)
```

Out[3]:

In [4]:

```
negation_elim = Forall(A, Equals(A, FALSE), conditions=[Not(A)])
```

Out[4]:

In [5]:

```
operand_is_bool = Forall(A, in_bool(A), condition=in_bool(Not(A)))
```

Out[5]:

In [6]:

```
%end axioms
```