Absorption Laws of Boolean algebra

This document was originally written to have an Algebra of sets (Wikipedia) to use as a basis for theories which build upon a theory of sets (such as general topology), but it was decided that Boolean algebra would suffice for those, as it is virtually equivalent for our modest purposes.

So it was turned into a demonstration of an alternative axiomatization of Boolean algebra.

In our main formulation of Boolean algebra, we took the absoption laws as axioms, and proved the identity laws. Here, we will take the identity laws as axioms, and prove the absorption laws.

Commutative properties:

axiom (#or-comm)        or(A, B) = or(B, A)
axiom (#and-comm)       and(A, B) = and(B, A)

Associative properties:

axiom (#or-assoc)       or(A, or(B, C)) = or(or(A, B), C)
axiom (#and-assoc)      and(A, and(B, C)) = and(and(A, B), C)

Distributive properties:

axiom (#or-dist)        or(A, and(B, C)) = and(or(A, B), or(A, C))
axiom (#and-dist)       and(A, or(B, C)) = or(and(A, B), and(A, C))

Complement (these are really more like definitions of 1 and 0):

axiom (#or-comp)        or(A, not(A)) = 1
axiom (#and-comp)       and(A, not(A)) = 0

Identity laws:

axiom (#union-id)       or(A, 0) = A
axiom (#inter-id)       and(A, 1) = A

Our proof of the absorption laws will rely on the annihilation laws (what the Wikipedia article calls the domination laws), which in turn rely on the idempotency laws, so we prove all those laws first. (These proofs also appear in the Boolean algebra document. There may be a good way to DRY these up, and if so, it would be good to do so.)

theorem (#or-idemp)
    or(X, X) = X
proof
    X = X
    or(X, 0) = X
    or(X, and(X, not(X))) = X             [by #and-comp with A=X]
    and(or(X, X), or(X, not(X))) = X
    and(or(X, X), 1) = X
    or(X, X) = X
qed

theorem (#and-idemp)
    and(X, X) = X
proof
    X = X
    and(X, 1) = X
    and(X, or(X, not(X))) = X             [by #or-comp with A=X]
    or(and(X, X), and(X, not(X))) = X
    or(and(X, X), 0) = X
    and(X, X) = X
qed

theorem (#or-annihil)
    or(X, 1) = 1
proof
    1 = 1
    or(X, not(X)) = 1                     [by #or-comp with A=X]
    or(or(X, X), not(X)) = 1
    or(X, or(X, not(X))) = 1
    or(X, 1) = 1
qed

theorem (#and-annihil)
    and(X, 0) = 0
proof
    0 = 0
    and(X, not(X)) = 0                     [by #and-comp with A=X]
    and(and(X, X), not(X)) = 0
    and(X, and(X, not(X))) = 0
    and(X, 0) = 0
qed

And now we prove the absorption laws.

theorem (#or-absorp)
    A = or(A, and(A, B))
proof
    A = A
    A = and(A, 1)
    A = and(A, or(B, 1))                   [by #or-annihil with X=B]
    A = and(A, or(1, B))
    A = or(and(A, 1), and(A, B))
    A = or(A, and(A, B))
qed

theorem (#or-absorp)
    A = and(A, or(A, B))
proof
    A = A
    A = or(A, 0)
    A = or(A, and(B, 0))                   [by #and-annihil with X=B]
    A = or(A, and(0, B))
    A = and(or(A, 0), or(A, B))
    A = and(A, or(A, B))
qed