Axioms for the theory of proveit.logic.booleans

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 Boolean, TRUE, FALSE, Forall, Equals, NotEquals, Union, Set
from proveit import A
In [2]:
%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:

In [3]:
true_axiom = TRUE

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

In [4]:
bools_def = Equals(Boolean, Set(TRUE, FALSE))

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

In [5]:
false_not_true = NotEquals(FALSE, TRUE)

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

In [6]:
eq_true_intro = Forall(A, Equals(A, TRUE), conditions=[A])
In [7]:
eq_true_elim = Forall(A, A, conditions=[Equals(A, TRUE)])
In [8]:
%end axioms
These axioms may now be imported from the theory package: proveit.logic.booleans