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

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.

not_t = Equals(Not(TRUE), FALSE)

not_t:

not_f = Equals(Not(FALSE), TRUE)

not_f:

negation_elim = Forall(A, Equals(A, FALSE), conditions=[Not(A)])

negation_elim:

operand_is_bool = Forall(A, in_bool(A), condition=in_bool(Not(A)))

operand_is_bool:

%end axioms

These axioms may now be imported from the theory package: proveit.logic.booleans.negation