Axioms for the theory of proveit.logic.booleans

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 Boolean, TRUE, FALSE, Forall, Equals, NotEquals, Union, Set
from proveit import A

%begin axioms

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

The TRUE literal ($\top$) is itself a true statement as an axiom:

true_axiom = TRUE

true_axiom:

The set of booleans, $\mathbb{B}$, is the set containing only TRUE ($\top$) and FALSE ($\bot$):

bools_def = Equals(Boolean, Set(TRUE, FALSE))

bools_def:

TRUE ($\top$) and FALSE ($\bot$) are defined to be different from each other:

false_not_true = NotEquals(FALSE, TRUE)

false_not_true:

When an expression is a Judgment, it is equal to TRUE and vice-versa:

eq_true_intro = Forall(A, Equals(A, TRUE), conditions=[A])

eq_true_intro:

eq_true_elim = Forall(A, A, conditions=[Equals(A, TRUE)])

eq_true_elim:

%end axioms

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