logo

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

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
Defining axioms for theory 'proveit.logic.booleans.negation'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

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]:
not_t:
In [3]:
not_f = Equals(Not(FALSE), TRUE)
Out[3]:
not_f:
In [4]:
negation_elim = Forall(A, Equals(A, FALSE), conditions=[Not(A)])
Out[4]:
negation_elim:
In [5]:
operand_is_bool = Forall(A, in_bool(A), condition=in_bool(Not(A)))
Out[5]:
operand_is_bool:
In [6]:
%end axioms
These axioms may now be imported from the theory package: proveit.logic.booleans.negation