Theorems (or conjectures) for the theory of proveit.logic.booleans.negation

import proveit
# Prepare this notebook for defining the theorems of a theory:
%theorems_notebook # Keep this at the top following 'import proveit'.
from proveit.logic import Not, FALSE, Forall, Implies, Equals, TRUE, Or, NotEquals, Boolean, in_bool
from proveit import A, B
%begin theorems

Defining theorems for theory 'proveit.logic.booleans.negation'
Subsequent end-of-cell assignments will define theorems
'%end theorems' will finalize the definitions

not_false = Not(FALSE)

not_false (established theorem):

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

negation_intro (established theorem):

negation_contradiction = Forall(A, FALSE, conditions=[A, Not(A)])

negation_contradiction (established theorem):

untrue_from_negation = Forall(A, NotEquals(A, TRUE), conditions=[Not(A)])

untrue_from_negation (established theorem):

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

falsified_negation_intro (established theorem):

double_negation_intro = Forall(A, Not(Not(A)), conditions=[A])

double_negation_intro (established theorem):

double_negation_elim_lemma = Forall(A, A, conditions=[Not(Not(A))],
                                domain=Boolean)

double_negation_elim_lemma (conjecture with conjecture-based proof):

double_negation_elim = Forall(A, A, conditions=[Not(Not(A))])

double_negation_elim (conjecture with conjecture-based proof):

closure = Forall(A, in_bool(Not(A)), domain=Boolean)

closure (conjecture with conjecture-based proof):

double_neg_closure = Forall(A, in_bool(Not(Not(A))), domain=Boolean)

double_neg_closure (conjecture with conjecture-based proof):

double_negation_equiv = Forall(A, Equals(Not(Not(A)), A), domain=Boolean)

double_negation_equiv (conjecture with conjecture-based proof):

%end theorems

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