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([])
```

Out[2]:

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([Not(TRUE)])
```

Out[3]:

In [4]:

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

Out[4]:

In [5]:

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

Out[5]:

In [6]:

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

Out[6]:

**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([in_bool(A)])
```

Out[7]:

In [8]:

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

Out[8]:

In [9]:

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

Out[9]:

In [10]:

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

Out[10]:

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

Out[11]:

In [12]:

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

Out[12]:

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

.

In [13]:

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

Out[13]:

In [14]:

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

Out[14]:

We can also show the inverse is true.

In [15]:

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

Out[15]:

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

Out[16]:

In [17]:

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

Out[17]:

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

In [18]:

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

Out[18]:

Again, the inverse is also true.

In [19]:

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

Out[19]:

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([Not(A)])
```

Out[20]:

We can also prove the inverse.

In [21]:

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

Out[21]:

In [22]:

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

Out[22]:

In [23]:

```
%end demonstrations
```