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

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 Boolean, TRUE, FALSE, in_bool, Implies, Not, And, Or, Forall
from proveit.logic import Equals, NotEquals, InSet
from proveit import A, C, P, Q, PofA, QofA
from proveit.logic import PofTrue, PofFalse, QimplPofTrue, QimplPofFalse

%begin theorems

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

Comparisons between Boolean values

true_eq_true = Equals(TRUE, TRUE)

true_eq_true (established theorem):

false_eq_false = Equals(FALSE, FALSE)

false_eq_false (established theorem):

true_not_false = NotEquals(TRUE, FALSE)

true_not_false (established theorem):

TRUE and FALSE are in the Boolean set:

fold_is_bool = Forall(A, in_bool(A), 
                    conditions=[Or(Equals(A, TRUE), Equals(A, FALSE))])

fold_is_bool (conjecture with conjecture-based proof):

true_is_bool = InSet(TRUE, Boolean)

true_is_bool (conjecture with conjecture-based proof):

false_is_bool = InSet(FALSE, Boolean)

false_is_bool (conjecture with conjecture-based proof):

in_bool_if_true = Forall(A, in_bool(A), conditions=[A])

in_bool_if_true (conjecture with conjecture-based proof):

in_bool_if_false = Forall(A, in_bool(A), conditions=[Not(A)])

in_bool_if_false (conjecture with conjecture-based proof):

not_equals_false = Forall(A, NotEquals(A, FALSE), conditions=[A])

not_equals_false (established theorem):

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

not_equals_true (established theorem):

Must equal TRUE or FALSE if in the Boolean set:

The first form of 'unfold' is a more direct consequence of the Boolean definition. See also 'unfold_is_bool'.

unfold_is_bool_explicit = Forall(A, Or(Equals(A, TRUE), Equals(A, FALSE)), domain=Boolean)

unfold_is_bool_explicit (conjecture with conjecture-based proof):

Folding $\forall$ over the Boolean domain

forall_over_bool_by_cases = Forall(P, Forall(A, PofA, domain=Boolean), conditions=[PofTrue, PofFalse])

forall_over_bool_by_cases (conjecture with conjecture-based proof):

conditioned_forall_over_bool_by_cases = Forall((P, Q), Forall(A, PofA, domain=Boolean, 
                                                              conditions=[QofA]), 
                                               conditions=[QimplPofTrue, QimplPofFalse])

conditioned_forall_over_bool_by_cases (conjecture with conjecture-based proof):

from_not_false = Forall(A, A, conditions=[NotEquals(A, FALSE)], domain=Boolean)

from_not_false (established theorem):

Evaluation of $\forall$ over the Boolean domain

forall_bool_eval_true = Forall(P, Equals(Forall(A, PofA, domain=Boolean), TRUE),
                           conditions=[Equals(PofTrue, TRUE), Equals(PofFalse, TRUE)])

forall_bool_eval_true (conjecture without proof):

unfold_forall_over_bool = Forall(P, Implies(Forall(A, PofA, domain=Boolean), 
                                         And(PofTrue, PofFalse)))

unfold_forall_over_bool (conjecture without proof):

Various ways for a $\forall$ expression over the Boolean set to evaluate to FALSE:

def _forallBoolEvalFalse(PofTrueVal, PofFalseVal):
    return Forall(P, Implies(And(Equals(PofTrue, PofTrueVal), Equals(PofFalse, PofFalseVal)), 
                             Equals(Forall(A, PofA, domain=Boolean), FALSE)))

forall_bool_eval_false_via_f_f = _forallBoolEvalFalse(FALSE, FALSE)

forall_bool_eval_false_via_f_f (conjecture without proof):

forall_bool_eval_false_via_f_t = _forallBoolEvalFalse(FALSE, TRUE)

forall_bool_eval_false_via_f_t (conjecture without proof):

forall_bool_eval_false_via_t_f = _forallBoolEvalFalse(TRUE, FALSE)

forall_bool_eval_false_via_t_f (conjecture without proof):

Must be a true statement or a false statement if in the Boolean set:

The second form, known as the 'law of excluded middle' can be more useful for unfolding the meaning of being in the Boolean set

in_bool_def = Forall(A, Equals(in_bool(A), Or(Equals(A, TRUE), Equals(A, FALSE))))

in_bool_def (conjecture with conjecture-based proof):

unfold_is_bool = Forall(A, Or(A, Not(A)), domain=Boolean)

unfold_is_bool (conjecture with conjecture-based proof):

from_excluded_middle = Forall(C, Forall(A, C, domain=Boolean,
                                            conditions=[Implies(A, C),
                                                        Implies(Not(A), C)]))

from_excluded_middle (conjecture with conjecture-based proof):

New facts may be derived via the 'law of excluded middle' through dual implications

The claim that $x\in \mathbb{B}$ should itself be in $\mathbb{B}$

in_bool_is_bool = Forall(A, in_bool(in_bool(A)))

in_bool_is_bool (conjecture with conjecture-based proof):

%end theorems

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