Between order and logic

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.

1. Preorders

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 ≼ b$ , $a ⋠ b$ (for $a, b \in X$ ) and $⊥$ . The rules are

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

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 $X$ , 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 $f : X \to S$ and a (non-strict) partial order $⩽$ on $S$ say that $a ≼ b$ is true via $f$ and $(S, ⩽)$ if $f (a) ⩽ f (b)$ ; and that $a ⋠ b$ is true via $f$ and $(S, ⩽)$ if $f (a) f (b)$ . $Σ ⊨ σ$ means that, for all $f$ , $(S, ⩽)$ , if these make all $τ \in Σ$ true then they make $σ$ true. With these semantics we have,

Theorem.

If $Σ ⊢ σ$ then $Σ ⊨ σ$ .

Theorem.

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 $X$ using $Σ^{+}$ . Then a partial order can be obtained by factoring out by the equivalence relation in Exercise 2.24.

2. Lattices

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 $LT (X)$ (lattice terms in $X$ ) to be the smallest set of strings of symbols from $\land$ , $\lor$ , $($ , $)$ and $a$ for each $a \in X$ such that:

each $a$ in $X$ is in $LT (X)$
if $s, t$ are in $LT (X)$ then so is $(s \land t)$
if $s, t$ are in $LT (X)$ then so is $(s \lor t)$

Given a function $f : X \to S$ where $(S, ⩽)$ is a lattice, we extend $f$ to $LT (X)$ by $f (s \land t) = f (s) \land f (t)$ and $f (s \lor t) = f (s) \lor f (t)$ .

Given $f : X \to S$ where $(S, ⩽)$ is a lattice, and $s ≼ t$ or $s ⋠ t$ we say that this sentence is true via $f$ and $(S, ⩽)$ if $f (s) ⩽ f (t)$ or $f (s) f (t)$ is, respectively.

We write $Σ ⊨ σ$ to mean that when even $f : X \to S$ and $(S, ⩽)$ is a lattice, if $f$ makes each $τ \in Σ$ true then it makes $σ$ true.

We now imagine a formal system where the wffs are $s ≼ t$ or $s ⋠ t$ or $⊥$ with $s, t \in LT (X)$ and rules as in the previous section for preorders (with $a, b, c$ ranging over $LT (X)$ this time) and also

from $s ≼ t$ deduce $(s \land r) ≼ t$
from $s ≼ t$ deduce $(r \land s) ≼ t$
from $s ≼ t$ and $s ≼ r$ deduce $s ≼ (t \land r)$
from $s ≼ t$ deduce $s ≼ (t \lor r)$
from $s ≼ t$ deduce $s ≼ (r \lor t)$
from $s ≼ t$ and $r ≼ t$ deduce $(s \lor r) ≼ t$

Theorem.

If $Σ ⊢ σ$ then $Σ ⊨ σ$ .

Theorem.

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 $X$ which is made into a lattice making $Σ^{+}$ true by factoring out by the equivalence relation in Exercise 2.24.

3. Distributive Lattices

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.

4. Boolean Algebras

The system in the previous section can be extended to boolean algebras too by adding $\neg$ . 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.