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 Boolean, TRUE, FALSE, Forall, Equals, NotEquals, Union, Set
from proveit import A
```

In [2]:

```
%begin axioms
```

**The TRUE literal ($\top$) is itself a true statement as an axiom:**

In [3]:

```
true_axiom = TRUE
```

**The set of booleans, $\mathbb{B}$, is the set containing only TRUE ($\top$) and FALSE ($\bot$):**

In [4]:

```
bools_def = Equals(Boolean, Set(TRUE, FALSE))
```

`TRUE`

($\top$) and `FALSE`

($\bot$) are defined to be different from each other:

In [5]:

```
false_not_true = NotEquals(FALSE, TRUE)
```

**When an expression is a Judgment, it is equal to TRUE and vice-versa:**

In [6]:

```
eq_true_intro = Forall(A, Equals(A, TRUE), conditions=[A])
```

In [7]:

```
eq_true_elim = Forall(A, A, conditions=[Equals(A, TRUE)])
```

In [8]:

```
%end axioms
```