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

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 Equals, NotEquals,Implies, TRUE, FALSE, Iff, Forall, And, Not, in_bool, Boolean
from proveit import A, B, C
%begin theorems

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

self_implication = Forall(A, Implies(A, A))

self_implication (established theorem):

true_implies_true = Implies(TRUE, TRUE)

true_implies_true (established theorem):

false_implies_false = Implies(FALSE, FALSE)

false_implies_false (established theorem):

false_implies_true = Implies(FALSE, TRUE)

false_implies_true (established theorem):

implies_t_t = Equals(Implies(TRUE, TRUE), TRUE)

implies_t_t (established theorem):

implies_f_f = Equals(Implies(FALSE, FALSE), TRUE)

implies_f_f (established theorem):

implies_f_t = Equals(Implies(FALSE, TRUE), TRUE)

implies_f_t (established theorem):

true_implies_false_negated = Not(Implies(TRUE, FALSE))

true_implies_false_negated (established theorem):

false_antecedent_implication = Forall(A, Implies(FALSE, A), domain=Boolean)

false_antecedent_implication (established theorem):

falsified_antecedent_implication = Forall((A, B), Implies(A, B), condition=Not(A))

falsified_antecedent_implication (established theorem):

untrue_antecedent_implication = Forall((A, B), Implies(A, B), condition=NotEquals(A, TRUE))

untrue_antecedent_implication (established theorem):

invalid_implication = Forall((A, B), Not(Implies(A, B)), conditions=[A, Not(B)])

invalid_implication (conjecture without proof):

not_true_via_contradiction = Forall(A, NotEquals(A,TRUE), conditions=Implies(A,FALSE))

not_true_via_contradiction (established theorem):

implication_transitivity = Forall((A, B, C), Implies(A, C), conditions=[Implies(A, B), Implies(B, C)])

implication_transitivity (established theorem):

modus_tollens_affirmation = Forall(A, Forall(B, A, conditions=[Implies(Not(A), B), Not(B)]), domain=Boolean)

modus_tollens_affirmation (established theorem):

modus_tollens_denial = Forall(A, Forall(B, Not(A), conditions=[Implies(A, B), Not(B)]), domain=Boolean)

modus_tollens_denial (established theorem):

negated_reflex = Forall((A,B), Implies(B,A), condition=Not(Implies(A,B)))

negated_reflex (established theorem):

iff_intro = Forall((A, B), Iff(A, B), conditions=[Implies(A, B), Implies(B, A)])

iff_intro (established theorem):

iff_via_both_true = Forall((A, B), Iff(A, B), conditions=[A, B])

iff_via_both_true (established theorem):

iff_via_both_false = Forall((A, B), Iff(A, B), 
                            conditions=[Not(A), Not(B)])

iff_via_both_false (conjecture without proof):

not_iff_via_not_right_impl = Forall((A, B), Not(Iff(A, B)), condition=Not(Implies(A, B)))

not_iff_via_not_right_impl (established theorem):

not_iff_via_not_left_impl = Forall((A, B), Not(Iff(A, B)), condition=Not(Implies(B, A)))

not_iff_via_not_left_impl (established theorem):

not_iff_via_not_right = Forall((A, B), Not(Iff(A, B)), conditions=[A, Not(B)])

not_iff_via_not_right (conjecture without proof):

not_iff_via_not_left = Forall((A, B), Not(Iff(A, B)), conditions=[Not(A), B])

not_iff_via_not_left (conjecture without proof):

true_iff_true = Iff(TRUE, TRUE)

true_iff_true (established theorem):

iff_t_t = Equals(Iff(TRUE, TRUE), TRUE)

iff_t_t (established theorem):

false_iff_false = Iff(FALSE, FALSE)

false_iff_false (established theorem):

iff_f_f = Equals(Iff(FALSE, FALSE), TRUE)

iff_f_f (established theorem):

iff_t_f = Equals(Iff(TRUE, FALSE), FALSE)

iff_t_f (established theorem):

true_iff_false_negated = Not(Iff(TRUE, FALSE))

true_iff_false_negated (established theorem):

iff_f_t = Equals(Iff(FALSE, TRUE), FALSE)

iff_f_t (established theorem):

false_iff_true_negated = Not(Iff(FALSE, TRUE))

false_iff_true_negated (established theorem):

iff_implies_right = Forall((A, B), Implies(A, B), conditions=[Iff(A, B)])

iff_implies_right (established theorem):

iff_implies_left = Forall((A, B), Implies(B, A), conditions=[Iff(A, B)])

iff_implies_left (established theorem):

right_from_iff = Forall((A, B), B, conditions=[A, Iff(A, B)])

right_from_iff (established theorem):

left_from_iff = Forall((A, B), A, conditions=[Iff(A, B), B])

left_from_iff (established theorem):

iff_symmetry = Forall((A, B), Iff(B, A), conditions=[Iff(A, B)])

iff_symmetry (established theorem):

iff_transitivity = Forall((A, B, C), Iff(A, C), conditions=[Iff(A, B), Iff(B, C)])

iff_transitivity (established theorem):

from_contraposition = Forall((A, B), Implies(A, B), conditions=[Implies(Not(B), Not(A)), in_bool(B)])

from_contraposition (established theorem):

to_contraposition = Forall((A, B), Implies(Not(B), Not(A)), conditions=[Implies(A, B), in_bool(A)])

to_contraposition (established theorem):

contrapose_neg_antecedent = Forall((A, B), Implies(Not(B), A), conditions=[Implies(Not(A), B), in_bool(A)])

contrapose_neg_antecedent (established theorem):

contrapose_neg_consequent = Forall((A, B), Implies(B, Not(A)), conditions=[Implies(A, Not(B)), in_bool(A)])

contrapose_neg_consequent (established theorem):

double_negate_consequent = Forall((A, B), Implies(A, Not(Not(B))), conditions=[Implies(A, B)])

double_negate_consequent (established theorem):

eq_from_iff = Forall((A, B), Equals(A, B), conditions=[Iff(A, B)], domain=Boolean)

eq_from_iff (conjecture with conjecture-based proof):

eq_from_mutual_impl = Forall((A, B), Equals(A, B), conditions=[Implies(A, B), Implies(B, A)], domain=Boolean)

eq_from_mutual_impl (conjecture with conjecture-based proof):

implication_closure = Forall((A, B), in_bool(Implies(A, B)), domain=Boolean)

implication_closure (conjecture with conjecture-based proof):

iff_closure = Forall((A, B), in_bool(Iff(A, B)), domain=Boolean)

iff_closure (conjecture with conjecture-based proof):

%end theorems

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