Context: proveit.logic.boolean

Boolean arithmetic. Booleans ($\mathbb{B}$) is the set containing only TRUE ($\top$) and FALSE ($\bot$). This context contains operations that are defined to act on Boolean elements: implication ($\Rightarrow$, $\Leftrightarrow$), negation ($\neg$), conjunction ($\land$), and disjunction ($\lor$). The quantification operations, universal ($\forall$) and existential ($\exists$), are also defined in this context because these operate on multiple instances of Booleans.

In [1]:
import proveit
common expressions axioms theorems demonstrations
implicationImplies and Iff (if and only if) operations
negationNot operation
conjunctionAnd operation
disjunctionOr operation
quantificationForall (universal quantification) and Exists (existential quantification) operations