logo

Demonstrations for the theory of proveit.logic.booleans.negation

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

The Boolean Set

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

Boolean Operations

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)
n_aeq_f:
In [12]:
n_aeq_f.prove(assumptions=[A])
 ⊢  

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

In [13]:
AeqF = Equals(A,FALSE)
AeqF:
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)
AneqT:
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