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
investigations.

Let us first consider a system for preorders and non-strict partial orders on a set $X$, extending Exercise 4.23. The wffs of the system are $a\preccurlyeq b$, $a\u22e0b$ (for $a,b\in X$) and $\perp $. The rules are

- The Given rule
- The RAA rule
- Reflexivity: if $a\in X$ then $a\preccurlyeq a$ can be written down at any time
- Transitivity: from $a\preccurlyeq b$ and $b\preccurlyeq c$ one may deduce $a\preccurlyeq c$
- Contradiction: from $a\preccurlyeq b$ and $a\u22e0b$ one may deduce $\perp $

There are two possible semantics for the system.

The first is the *preorder semantics*
we define when a statement is true in a preorder $\u2a7d$ on $X$, and
define semantics accordingly, as in Chapter 4, but for $\u2a7d$ and $\preccurlyeq $
instead of $<$ and $\prec $. (Exercise: state and prove a completeness and
soundness theorem for this semantics.)

The second is a bit more interesting. Given a function $f:X\to S$ and a (non-strict) partial order $\u2a7d$ on $S$ say that $a\preccurlyeq b$ is true via $f$ and $(S,\u2a7d)$ if $f\left(a\right)\u2a7df\left(b\right)$; and that $a\u22e0b$ is true via $f$ and $(S,\u2a7d)$ if $f\left(a\right)f\left(b\right)$. $\Sigma \models \sigma $ means that, for all $f$, $(S,\u2a7d)$, if these make all $\tau \in \Sigma $ true then they make $\sigma $ true. With these semantics we have,

Theorem.

If $\Sigma \u22a2\sigma $ then $\Sigma \models \sigma $.

Theorem.

If $\Sigma \models \sigma $ then $\Sigma \u22a2\sigma $.

The proof of the completeness theorem goes by assuming $\Sigma \u22ac\perp $, taking (by Zorn's lemma) a maximal consistent extension ${\Sigma}^{+}$ of $\Sigma $ and defining a preorder on $X$ using ${\Sigma}^{+}$. 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 $X$ we define $\text{LT}\left(X\right)$ (lattice terms in $X$) to be the smallest set of strings of symbols from $\wedge $, $\vee $, $($, $)$ and $a$ for each $a\in X$ such that:

- each $a$ in $X$ is in $\text{LT}\left(X\right)$
- if $s,t$ are in $\text{LT}\left(X\right)$ then so is $(s\wedge t)$
- if $s,t$ are in $\text{LT}\left(X\right)$ then so is $(s\vee t)$

Given a function $f:X\to S$ where $(S,\u2a7d)$ is a lattice, we extend $f$ to $\text{LT}\left(X\right)$ by $f(s\wedge t)=f\left(s\right)\wedge f\left(t\right)$ and $f(s\vee t)=f\left(s\right)\vee f\left(t\right)$.

Given $f:X\to S$ where $(S,\u2a7d)$ is a lattice, and $s\preccurlyeq t$ or $s\u22e0t$ we say that this sentence is true via $f$ and $(S,\u2a7d)$ if $f\left(s\right)\u2a7df\left(t\right)$ or $f\left(s\right)f\left(t\right)$ is, respectively.

We write $\Sigma \models \sigma $ to mean that when even $f:X\to S$ and $(S,\u2a7d)$ is a lattice, if $f$ makes each $\tau \in \Sigma $ true then it makes $\sigma $ true.

We now imagine a formal system where the wffs are $s\preccurlyeq t$ or $s\u22e0t$ or $\perp $ with $s,t\in \text{LT}\left(X\right)$ and rules as in the previous section for preorders (with $a,b,c$ ranging over $\text{LT}\left(X\right)$ this time) and also

- from $s\preccurlyeq t$ deduce $(s\wedge r)\preccurlyeq t$
- from $s\preccurlyeq t$ deduce $(r\wedge s)\preccurlyeq t$
- from $s\preccurlyeq t$ and $s\preccurlyeq r$ deduce $s\preccurlyeq (t\wedge r)$
- from $s\preccurlyeq t$ deduce $s\preccurlyeq (t\vee r)$
- from $s\preccurlyeq t$ deduce $s\preccurlyeq (r\vee t)$
- from $s\preccurlyeq t$ and $r\preccurlyeq t$ deduce $(s\vee r)\preccurlyeq t$

Theorem.

If $\Sigma \u22a2\sigma $ then $\Sigma \models \sigma $.

Theorem.

If $\Sigma \models \sigma $ then $\Sigma \u22a2\sigma $.

Again, the proof of the completeness theorem is by supposing that $\Sigma \u22ac\perp $, choosing a maximally consistent ${\Sigma}^{+}$ extending $\Sigma $ and showing that ${\Sigma}^{+}$ defines a preorder on $X$ which is made into a lattice making ${\Sigma}^{+}$ 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 $\neg $.
However, at this point the inequality $\preccurlyeq $ 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.