Axiomatizing Boolean Algebras
The technique we just used to prove an identity of Boolean algebra can be generalized to all identities in a systematic way that can be taken as a sound and complete axiomatization of, or axiomatic system for, the equational laws of Boolean logic. The customary formulation of an axiom system consists of a set of axioms that "prime the pump" with some initial identities, along with a set of inference rules for inferring the remaining identities from the axioms and previously proved identities. In principle it is desirable to have finitely many axioms; however as a practical matter it is not necessary since it is just as effective to have a finite axiom schema having infinitely many instances each of which when used in a proof can readily be verified to be a legal instance, the approach we follow here.
Boolean identities are assertions of the form s = t where s and t are n-ary terms, by which we shall mean here terms whose variables are limited to x0 through xn-1. An n-ary term is either an atom or an application. An application mfi(t0,…,tm-1) is a pair consisting of an m-ary operation mfi and a list or m-tuple (t0,…,tm-1) of m n-ary terms called operands.
Associated with every term is a natural number called its height. Atoms are of zero height, while applications are of height one plus the height of their highest operand.
Now what is an atom? Conventionally an atom is either a constant (0 or 1) or a variable xi where 0 ≤ i < n. For the proof technique here it is convenient to define atoms instead to be n-ary operations nfi, which although treated here as atoms nevertheless mean the same as ordinary terms of the exact form nfi(x0,…,xn-1) (exact in that the variables must listed in the order shown without repetition or omission). This is not a restriction because atoms of this form include all the ordinary atoms, namely the constants 0 and 1, which arise here as the n-ary operations nf0 and nf−1 for each n (abbreviating 22n−1 to −1), and the variables x0,…,xn-1 as can be seen from the truth tables where x0 appears as both the unary operation 1f2 and the binary operation 2f10 while x1 appears as 2f12.
The following axiom schema and three inference rules axiomatize the Boolean algebra of n-ary terms.
- A1. mfi(nfj0,…,nfjm-1) = nfioĵ where (iĵ)v = iĵv, with ĵ being j transpose, defined by (ĵv)u = (ju)v.
- R1. With no premises infer t = t.
- R2. From s = u and t = u infer s = t where s, t, and u are n-ary terms.
- R3. From s0 = t0,…,sm-1 = tm-1 infer mfi(s0,…,sm-1) = mfi(t0,…,tm-1), where all terms si, ti are n-ary.
The meaning of the side condition on A1 is that iĵ is that 2n-bit number whose v-th bit is the ĵv-th bit of i, where the ranges of each quantity are u: m, v: 2n, ju: 22n, and ĵv: 2m. (So j is an m-tuple of 2n-bit numbers while ĵ as the transpose of j is a 2n-tuple of m-bit numbers. Both j and ĵ therefore contain m2n bits.)
A1 is an axiom schema rather than an axiom by virtue of containing metavariables, namely m, i, n, and j0 through jm-1. The actual axioms of the axiomatization are obtained by setting the metavariables to specific values. For example if we take m = n = i = j0 = 1, we can compute the two bits of iĵ from i1 = 0 and i0 = 1, so iĵ = 2 (or 10 when written as a two-bit number). The resulting instance, namely 1f1(1f1) = 1f2, expresses the familiar axiom ¬¬x = x of double negation. Rule R3 then allows us to infer ¬¬¬x = ¬x by taking s0 to be 1f1(1f1) or ¬¬x0, t0 to be 1f2 or x0, and mfi to be 1f1 or ¬.
For each m and n there are only finitely many axioms instantiating A1, namely 22m × (22n)m. Each instance is specified by 2m+m2n bits.
We treat R1 as an inference rule, even though it is like an axiom in having no premises, because it is a domain-independent rule along with R2 and R3 common to all equational axiomatizations, whether of groups, rings, or any other variety. The only entity specific to Boolean algebras is axiom schema A1. In this way when talking about different equational theories we can push the rules to one side as being independent of the particular theories, and confine attention to the axioms as the only part of the axiom system characterizing the particular equational theory at hand.
This axiomatization is complete, meaning that every Boolean law s = t is provable in this system. One first shows by induction on the height of s that every Boolean law for which t is atomic is provable, using R1 for the base case (since distinct atoms are never equal) and A1 and R3 for the induction step (s an application). This proof strategy amounts to a recursive procedure for evaluating s to yield an atom. Then to prove s = t in the general case when t may be an application, use the fact that if s = t is an identity then s and t must evaluate to the same atom, call it u. So first prove s = u and t = u as above, that is, evaluate s and t using A1, R1, and R3, and then invoke R2 to infer s = t.
In A1, if we view the number nm as the function type m→n, and mn as the application m(n), we can reinterpret the numbers i, j, ĵ, and iĵ as functions of type i: (m→2)→2, j: m→((n→2)→2), ĵ: (n→2)→(m→2), and iĵ: (n→2)→2. The definition (iĵ)v = iĵv in A1 then translates to (iĵ)(v) = i(ĵ(v)), that is, iĵ is defined to be composition of i and ĵ understood as functions. So the content of A1 amounts to defining term application to be essentially composition, modulo the need to transpose the m-tuple j to make the types match up suitably for composition. This composition is the one in Lawvere's previously mentioned category of power sets and their functions. In this way we have translated the commuting diagrams of that category, as the equational theory of Boolean algebras, into the equational consequences of A1 as the logical representation of that particular composition law.
Read more about this topic: Boolean Algebras Canonically Defined