A Formalization of the Boole-Schröder Algebra in Coq
====================================================

As an exercise in learning how to use the Coq proof assistant, I picked up a book on symbolic logic (Symbolic Logic: Clarance Irving Lewis & Cooper Harold Langford, 1959) and decided to try to formalize the Boole-Schröder algebra using it as a guide. I found the book for pennies at Second Story Books at their Rockville warehouse store (meanwhile the going rate on Amazon for actual copies of the book is hundreds of dollars). It was among a number of old math books on logic and computing I got for cheap.

Foundations
-----------

Boole-Schröder algebra, more commonly known as boolean algebra, was conceived by Ernst Schröder as an extension of George Boole’s Logic. It deals with propositions, which can represent two different kinds of things: assserting a relation between the concepts that the terms of an expression connote, or between the classes that the terms denote. The connotation of terms refers to relationships between concepts, such as the concept “man” implying the concept “mortal”. The denotation of terms refers to relationships between classes, such as the class “man” being contained within the class “mortal”. You can roughly interpret this as the difference between the terms representing statements that are either true or false and sets.

The algebra is constructed from the following assumptions:

  1. Any ‘term’ (a, b, etc.) will represent some class of things, named by some logical term.
  2. a ⨯ b (or a b): what is common to a and b.
  3. -a: not (or inverse of) a.
  4. 0: nothing (null class).
  5. a = b means the terms have the same extension (class).

And the following definitions (book’s numbering system used):

And the following postulates:

What I’ve just listed is the entirety of boolean algebra. All further laws can be derived from these assumptions, definitions, and postulates.

Foundations in Coq
------------------

We can now construct our BooleSchroderAlgebra Coq class and assign some notation.

Class BooleSchroderAlgebra (A : Type) := {
  zero : A;  (* null class *)
  one : A;  (* universe of discourse class *)
  union : A -> A -> A;
  inter : A -> A -> A;
  neg : A -> A;
  contains : A -> A -> Prop;
  
  (* 1.01 *) neg_zero : neg zero = one;
  (* 1.01 *) neg_one : neg one = zero;
  (* 1.02 *) union_def : forall a b, union a b = neg(inter (neg a) (neg b));
  (* 1.03 *) contains_def : forall a b, contains a b <-> inter a b = a;
  
  (* 1.1 *) inter_identity : forall a, inter a a = a;
  (* 1.2 *) inter_comm : forall a b, inter a b = inter b a;
  (* 1.3 *) inter_assoc : forall a b c, inter a (inter b c) = inter (inter a b) c;
  (* 1.4 *) inter_zero : forall a, inter a zero = zero;
  (* 1.5 *) inter_neg_zero_contains : forall a b, inter a (neg b) = zero <-> contains a b;
  (* 1.6 *) contains_zero : forall a b, contains a b /\ contains a (neg b) <-> a = zero;
}.

Infix "∪" := union (at level 50, left associativity).
Infix "∩" := inter (at level 40, left associativity).
Notation "¬ x" := (neg x) (at level 35, right associativity).
Infix "⊂" := contains (at level 70, no associativity).

Our definitions and postulates specified in the Coq class are assumed true by Coq for theorems using terms from that class. Borrowing from set theory, a + b is represented with the notation a ∪ b, a b is represented with the notation a ∩ b, and -a is represented with the notation ¬ a.

The type signatures of most of the operations are pretty self-explanatory. However, one stands out in particular: contains. Its type is given as A -> A -> Prop. I stated earlier that this algebra deals with propositions expressed by relations between terms. While all the other operators take terms and yield a term, contains takes terms and yields a proposition. It’s kind of a meta-proposition, since the terms themselves can be propositions, but not on the same level. Possibly counter-intuitively, it’s improper to write something like a = b ⊂ c, because it would be nonsensical when the terms denote classes rather than connote propositional concepts (not all concepts are propositional). The = operator in Coq also has the type A -> A -> Prop, but it is provided for us as a built-in convenience so we don’t need to re-define it.

Proving Theorems
----------------

From here, we can start proving various theorems. So far, I have translated 13 of the book’s proofs into Coq proofs, and I have posted them at https://gist.github.com/lisanna-dettwyler/3f26328097c0a7fb8c4fa4e993c5b143. The theorems as given in the book are pictured above.

I have found this to be a useful way to practice writing proofs in Coq. Since the proofs in this book tend to be on the terser side, you really have to think through each step carefully to not miss anything, as what can be implied on paper cannot be implied with a machine.

· coq