Paul Halmos's name for this algebra "2" has some following in the literature, and will be employed here.
Sum and product commute and associate, as in the usual algebra of real numbers.
Either one-to-one correspondence between {0,1} and {True,False} yields classical bivalent logic in equational form, with complementation read as NOT.
2 can be seen as grounded in the following trivial "Boolean" arithmetic: Note that: This Boolean arithmetic suffices to verify any equation of 2, including the axioms, by examining every possible assignment of 0s and 1s to each variable (see decision procedure).
For this and other reasons, a sum of products (leading to a NAND synthesis) is more commonly employed than a product of sums (leading to a NOR synthesis).
Each of '+' and '∙' can be defined in terms of the other and complementation: We only need one binary operation, and concatenation suffices to denote it.
This basis makes for an easy approach to proof, called "calculation" in Laws of Form, that proceeds by simplifying expressions to 0 or 1, by invoking axioms (2)–(4), and the elementary identities
De Morgan's theorem states that if one does the following, in the given order, to any Boolean function: the result is logically equivalent to what you started with.
Repeated application of De Morgan's theorem to parts of a function can be used to drive all complements down to the individual variables.
A powerful and nontrivial metatheorem states that any identity of 2 holds for all Boolean algebras.
Whether there exists a decision procedure whose steps are a polynomial function of N falls under the P = NP conjecture.
The above metatheorem does not hold if we consider the validity of more general first-order logic formulas instead of only atomic positive equalities.
The decidability for the first-order theory of many classes of Boolean algebras can still be shown, using quantifier elimination or small model property (with the domain size computed as a function of the formula and generally larger than 2).
Many elementary texts on Boolean algebra were published in the early years of the computer era.
Perhaps the best of the lot, and one still in print, is: The following items reveal how the two-element Boolean algebra is mathematically nontrivial.