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

In [1]:
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
In [2]:
implies_t_f = Equals(Implies(TRUE, FALSE), FALSE)
In [3]:
affirmation_via_contradiction = Forall(A, A, domain=Boolean, conditions=[Implies(Not(A), FALSE)])
In [4]:
denial_via_contradiction = Forall(A, Not(A), domain=Boolean, conditions=[Implies(A, FALSE)])

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

In [5]:
iff_def = Forall((A, B), Equals(Iff(A, B), And(Implies(A, B), Implies(B, A))))
In [6]:
%end axioms
These axioms may now be imported from the theory package: proveit.logic.booleans.implication