Theory of proveit.logic.booleans¶

Boolean arithmetic. Boolean ($\mathbb{B}$) is the set containing only TRUE ($\top$) and FALSE ($\bot$). This theory 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 theory because these operate on multiple instances of Boolean values.

import proveit
%theory

Theory of proveit.logic.booleans¶

Local content of this theory

Sub-theories

All axioms contained within this theory

proveit.logic.booleans.implication

proveit.logic.booleans.negation

proveit.logic.booleans.conjunction

proveit.logic.booleans.disjunction

proveit.logic.booleans.quantification

implication	Implies and Iff (if and only if) operations
negation	Not operation
conjunction	And operation
disjunction	Or operation
quantification	Forall (universal quantification) and Exists (existential quantification) operations