There are a number of systems that might be said to exist between
the system for partial orders of Chapter 4 of
The Mathematics of Logic
and the propositional calculus of Chapter 6, systems that correspond in some way to
the algebraic ideas (lattices, distributive lattices, etc) discussed briefly
in Chapter 5. This web page contains some suggestions for the reader's
Let us first consider a system for preorders and non-strict partial orders on a set , extending Exercise 4.23. The wffs of the system are , (for ) and . The rules are
There are two possible semantics for the system.
The first is the preorder semantics we define when a statement is true in a preorder on , and define semantics accordingly, as in Chapter 4, but for and instead of and . (Exercise: state and prove a completeness and soundness theorem for this semantics.)
The second is a bit more interesting. Given a function and a (non-strict) partial order on say that is true via and if ; and that is true via and if . means that, for all , , if these make all true then they make true. With these semantics we have,
If then .
If then .
The proof of the completeness theorem goes by assuming , taking (by Zorn's lemma) a maximal consistent extension of and defining a preorder on using . Then a partial order can be obtained by factoring out by the equivalence relation in Exercise 2.24.
We now extend the system of the previous section to lattices, obtaining a nondistributive theory of AND and OR.
Given a set we define (lattice terms in ) to be the smallest set of strings of symbols from , , , and for each such that:
Given a function where is a lattice, we extend to by and .
Given where is a lattice, and or we say that this sentence is true via and if or is, respectively.
We write to mean that when even and is a lattice, if makes each true then it makes true.
We now imagine a formal system where the wffs are or or with and rules as in the previous section for preorders (with ranging over this time) and also
If then .
If then .
Again, the proof of the completeness theorem is by supposing that , choosing a maximally consistent extending and showing that defines a preorder on which is made into a lattice making true by factoring out by the equivalence relation in Exercise 2.24.
The system in the previous section can be extended to distributive lattices by adding rules for the distributive laws and redefining the semantics so that only distributive lattices are used. I've nothing much to add to this at the moment.
The system in the previous section can be extended to boolean algebras too by adding .
However, at this point the inequality can be dispensed with, as indicated in the very
beginning of Chapter 6 of
The Mathematics of Logic. The resulting system is Propositional logic,
as described in that chapter.