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

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

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

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

implies_t_f:

affirmation_via_contradiction = Forall(A, A, domain=Boolean, conditions=[Implies(Not(A), FALSE)])

affirmation_via_contradiction:

denial_via_contradiction = Forall(A, Not(A), domain=Boolean, conditions=[Implies(A, FALSE)])

denial_via_contradiction:

Iff (if and only if) is defined as implication in both directions:

iff_def = Forall((A, B), Equals(Iff(A, B), And(Implies(A, B), Implies(B, A))))

iff_def:

%end axioms

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