In [1]:

```
import proveit
from proveit import A, B, C
from proveit.logic import Not, Equals, NotEquals, TRUE, FALSE, Implies, in_bool, Boolean
%begin demonstrations
```

"Boolean" is a logical term used to denote a type of variable that has two possible values: `True`

or `False`

. Negation is the act of outputing the opposite of the original term.

True to the nature of members of the Boolean set, we can perform operations on `True`

and `False`

themselves.

In [2]:

```
Not(FALSE).prove()
```

Because we know that there are only two possible values in the Boolean set, the opposite or $\lnot$ of one value must produce the other.

In [3]:

```
FALSE.prove(assumptions=[Not(TRUE)])
```

In [4]:

```
Equals(Not(FALSE), TRUE).prove()
```

In [5]:

```
Equals(Not(TRUE), FALSE).prove()
```

In [6]:

```
Implies(Not(TRUE),FALSE).prove()
```

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

These next theorems prove what is implicit in the following axioms.

In [7]:

```
in_bool(Not(A)).prove(assumptions=[in_bool(A)])
```

In [8]:

```
in_bool(Not(Not(A))).prove(assumptions=[in_bool(A)])
```

In [9]:

```
in_bool(A).prove(assumptions=[in_bool(Not(A))])
```

In [10]:

```
Not(Not(A)).double_negation_equivalence(assumptions=[in_bool(A)]).prove()
```

Unless specifically defined otherwise, $A$'s default definition is `True`

. Therefore, since $A$ is `True`

, we can define $\lnot A$ as `False`

In [11]:

```
n_aeq_f = Equals(Not(A), FALSE)
```

In [12]:

```
n_aeq_f.prove(assumptions=[A])
```

Similarly, given $\lnot A$ we can show that $A$ = `False`

.

In [13]:

```
AeqF = Equals(A,FALSE)
```

In [14]:

```
AeqF.prove(assumptions=[Not(A)])
```

We can also show the inverse is true.

In [15]:

```
Not(A).prove(assumptions=[AeqF])
```

On the other hand, we can also show that $\lnot A$ is $\neq$ to `True`

because $A$ is equal to `True`

.

In [16]:

```
AneqT = NotEquals(A, TRUE)
```

In [17]:

```
AneqT.prove(assumptions=[Not(A)])
```

Similarly, the double negation negates the original negation, providing the original statement.

In [18]:

```
A.prove(assumptions=[Not(Not(A))])
```

Again, the inverse is also true.

In [19]:

```
Not(Not(A)).prove(assumptions=[A])
```

By going one step further, we can prove that three $\lnot$'s are the same as a single $\lnot$.

In [20]:

```
Not(Not(Not(A))).prove(assumptions=[Not(A)])
```

We can also prove the inverse.

In [21]:

```
Not(A).prove(assumptions=[Not(Not(Not(A)))])
```

In [22]:

```
Not(Not(B)).double_negation_equivalence(assumptions=[in_bool(B)])
```

In [23]:

```
%end demonstrations
```