The algebraic core of a propositional logic (with Rutger M. Dijkstra)

The algebraic core of a propositional logic

This note deals with the following theorem.

For a nonempty domain $E$ ,there exist the operators $\rightarrow$ of type ${E}^{2} \rightarrow E$ ,of type $E \rightarrow E$ ,and [...] of type $E \rightarrow$ bool. The prefix operator $\bullet$ is given a higher syntactic binding power than the infix $\rightarrow$ .

Universal quantification over $a,b,c$ is often left implicit. The operators satisfy

$[a \rightarrow (b \rightarrow a)]$ $[ (a \rightarrow (b \rightarrow c)) \rightarrow ((a \rightarrow b) \rightarrow (a \rightarrow c)) ]$ $(0,C)$ $[\cdot a\rightarrow b)\rightarrow ((\cdot a\rightarrow \cdot b)\rightarrow a)]$ [\left( {0,{MP}}\right) \quad \left\lbrack a\right\rbrack \land \left\lbrack {a \rightarrow b}\right\rbrack \Rightarrow \left\lbrack b\right\rbrack ]

(The four names are short for Weakening, Distribution, Contradiction and Modus Ponens respectively.)

In terms of the above we now define the relations $\varepsilon$ and $\approx$ , both of type $E^2 \rightarrow \mathrm{bool}$ :

(1) $a \leq b \equiv \left\lbrack {a \rightarrow b}\right\rbrack$ (2) $a \simeq b \equiv a \leq b \land b \leq a$

(In view of the types, no further binding powers need to be defined.)

Then

(i) $\subseteq$ is a preorder (i.e. is reflexive and transitive). (ii) $\rightarrow$ and "preserve $\approx$ " (see later) (iii) $\left( {E/ \cong ,E}\right)$ is a boolean lattice,i.e. there exist

operators ↑,↓,~ which "preserve ≅" and satisfy

(iii,supremum) $a \uparrow b \leq c \equiv a \leq c \land b \leq c$ (iii, infimum) ${a}{E}{b}{L}^{c} \equiv {a}{E}b \land {a}{E}c$ (iii, shuntg) $a \downarrow b \cong c \cong b \cong {a}^{\prime }c$

To begin with we rewrite the properties (0), introducing $\leq$ via (1):

$\left( {3,W}\right) \;a \leq b \sim a$ (3, 0) $\;a \rightarrow \left( {b \rightarrow c}\right) \leq \;\left( {a \rightarrow b}\right) \rightarrow \left( {a \rightarrow c}\right)$ (3,C) $\therefore a \sim b\;E\;\left( {\bullet a \sim \bullet b}\right) \sim a$ (3,MP) $a \leq b \Rightarrow \left( {\lbrack a\rbrack \Rightarrow \lbrack b\rbrack }\right)$

Note that in deriving (3,MP) we have also applied shunting from the predicate calculus; we have done so in order to express clearly that MP is a monotonicity property of [...] Note also that the above was just a rewriting: formulae (3) are equivalent to formulae (0).

Matching the 5 of (3,MP) with the s's in the preceding 3 properties, we derive, again via (1)

[\left\lbrack a\right\rbrack \Rightarrow b \leq a] $\left( {4,D}\right) \;a \in b \rightarrow c \Rightarrow a \rightarrow b \in a \rightarrow c$ [\left( {4,c}\right) \;a \leq b \Rightarrow - a \rightarrow b \leq a]

(Because (3,MP) is an implication, formulae (4) are weaker than the corresponding formulae (3).)

The consequents of formulae (4) have all the form of the antecedent of (3,MP), so we can use the latter again. Thus we derive (with shunting from the predicate calculus)

$(5, W)$ $[a] \wedge [b] \Rightarrow [a]$ $(5,0)$ $a \leq b \rightarrow c \wedge {a}{5}b \Rightarrow {a}{5}c$ $\left( {5,c}\right) \cdot {a}{5}b \land {a}{5}b \Rightarrow \left\lbrack a\right\rbrack$

Conclusion (5, W) gives us nothing new, (5, D) will be used in a moment, and (5, C) nicely reflects the Reductio ad Absurdum.

After the above explorations we are ready to tackle section (i) of our proof obligation.

$\underline{5}$ is reflexive , i.e. for any $a$

(6) $a \leq a$

Proof We observe

$$ a \leq a $$

$$ \Leftrightarrow {5, D) w i t h c := a } $$

$$ \langle \exists b:: a \leq b \rightarrow a \land a \leq b \rangle $$

$$ = {(3, w) } $$

$$ \langle \exists b:: a \leq b \rangle $$

$$ \Leftrightarrow {\mathrm {i n s t a n t i a t i o n} b := c \rightarrow a } $$

$$ \langle \exists c: a \leq c \rightarrow a \rangle $$

$$ \equiv {(3, w) a n d E n o n e m p h y } $$

$$ t r u e $$

(End of Proof.)

$\frac{5}{1}$ is transitive , i.e. for any $a,b,c$

(7) ${a5b} \land {b5c} \Rightarrow {a5c}$

Proof We observe for any $a,b,c$

$$ a \subseteq c $$

$$ \Leftrightarrow {(\mathbf {5}, \mathbf {D}) } $$

$$ a \leq b \land a \leq b \rightarrow c $$

$$ \Leftrightarrow {(\mathrm {8}), \mathrm {s e e b e l o w} } $$

$$ a \leq b \land b \leq c $$

(End of Proof.)

Above we have used

(8) $b \leq c \Rightarrow a \leq b \rightarrow c$

(which could deserve a number in its own right).

Proof We observe for any $a,b,c$

$$ a \le b \rightarrow c $$

$$ \Leftarrow \quad {(4, w) \mathrm {w i t h} a, b := b \rightarrow c, a } $$

$$ [ b \rightarrow c ] $$

$$ \equiv {() } $$

$$ b \le c $$

(End of Proof.)

Thanks to the reflexivity of $\equiv$ we derive

$\left( 9\right) \;b \rightarrow c) \rightarrow b \leq \left( {b \sim c}\right) \rightarrow c$

The transitivity of $\leq$ will be exploited by admitting $\varepsilon$ in the left column of our proof

format.

Finally we conclude from (2), (6) & (7):

(10) $a \simeq a$ i.e. $\simeq$ is reflexive

$$ \begin{array}{l} a \approx b \equiv b \approx a \quad i. e. \approx i s s y m m e t r i c \ a \approx b \land b \approx c \Rightarrow a \approx c \quad i. e. \approx i s t r a n s i t i v e, \ \end{array} $$

hence $\approx$ is an equivalence relation (as already suggested by the symbol chosen). Because of the transitivity, also $\approx$ can be admitted in the left column of our proof format.

This concludes the proof of (i) and our discussion of its immediate consequences.

The time has come to turn to proof obligation (ii) and we shall start with $\Rightarrow$ preserves $\cong$ , which is short for "the prefix operator $a \rightarrow$ preserves $\cong$ ", i.e.

(11) $b \simeq c \Rightarrow a \sim b \simeq a \sim c$

and "the postfix operator $\rightarrow c$ preserves $\approx$ ", i.e.

(12) $a \simeq b \Rightarrow a \sim c \simeq b \sim c$

By virtue of definition (2) of $\simeq$ , predicate calculus and symmetry, (11) follows from

(13,1) $b \subseteq c \Rightarrow a \rightarrow b \subseteq a \rightarrow c$

while, similarly, (12) follows from

(13,AM) $a \leq b \Rightarrow b \sim c \leq a \sim c\;$ .

(Here M and AM are short for Monotonicity and Anti-Monotonicity respectively.) formulae (13) follow via (3,MP) and definition (1) of $\varepsilon$ , directly from

$\left( {{14},M}\right) \;b \rightarrow c \leq \;\left( {a \rightarrow b}\right) \rightarrow \left( {a \rightarrow c}\right)$ and

(14,AM) $a \sim b \leq \left( {b \sim c}\right) \rightarrow \left( {a \sim c}\right)$

For the proof of (14,M) we observe

$$ b \rightarrow c $$

[\left{ {\left( {3,w}\right) \text{ with }a,b \mathrel{\text{:=}} b \rightarrow c,a}\right} ]

$$ a \rightarrow (b \rightarrow c) $$

[\left{ {\left( {3,\mathcal{D}}\right) }\right} ]

$$ (a \rightarrow b) \rightarrow (a \rightarrow c) $$

the transitivity of $\varepsilon$ then completes the proof.

For the proof of (14,AM) we observe

$$ a \rightarrow b \equiv (b \rightarrow c) \rightarrow (a \rightarrow c) $$

$\Leftrightarrow \left{ {\left( {3,W}\right) \text{ and transitivity of }E}\right}$

$$ (b \rightarrow c) \rightarrow (a \rightarrow b) \subseteq (b \rightarrow c) \rightarrow (a \rightarrow c) $$

[\left{ {\left( {4,0}\right) }\right} ]

$$ b \sim c \subseteq (a \sim b) \sim (a \sim c) $$

$\left{ {\left( {{14},M}\right) }\right}$

$$ \begin{array}{l} \text {t r u e} \ \hline \end{array} , $$

and this completes the proof that $\rightarrow$ preserves $\approx$ .

The antimonotonicity enables us to prove the useful shunting rules

$$ \begin{array}{l} (1 5, S) \quad a \rightarrow (b \rightarrow c) \approx b \rightarrow (a \rightarrow c) \ (1 6, S) \quad a \leq b \sim c \quad \equiv b \leq a \sim c \ \end{array} $$

The above two lemmata follow from the symmetry in $\mathbf{a},\mathbf{b}$ ,definitions (1) and (2),

$$ a \rightarrow (b \rightarrow c) \subseteq b \rightarrow (a \rightarrow c) $$

which is proved by observing

$$ a \rightarrow (b \rightarrow c) $$

$$ \begin{array}{l} \equiv {(3, D) } \ (a \rightarrow b) \rightarrow (a \rightarrow c) \ \equiv {\text {f r o m} (3, W) b \leq a \rightarrow b; (1 3, A M) } \ b \rightarrow (a \rightarrow c) \ \end{array} $$

We now turn to the remainder of proof obligation (ii), viz. that "preserves $\cong$ ". or formally

$$ a \simeq b \Rightarrow a \simeq b $$

This means that we have to use what has been given about $\bullet$ ,i.e. (0,C) or -equivalent and probably more convenient- (3,C). (It is probably unwise to found our further study of $\bullet$ on (4,C),as that is intrinsically weaker.) Our recent result (16,S) about shunting allows us to rewrite

(3,c) $\therefore a \rightarrow b \leq \left( {\bullet a \rightarrow \bullet b}\right) \rightarrow a$

as

(17,c) $\; \cdot a \rightarrow \;b \leq \left( {a \rightarrow b}\right) \rightarrow a\;,\;$

i.e. the fundamental property of $\bullet$ is symmetric in $b$ and $\bullet b$ . (Since we hope to show that $\bullet$ is its own inverse, this is very encouraging.)

We now observe for any $a, b$

true

[\left{ {\left( {3,c}\right) }\right} ] $\therefore a \rightarrow b \leq \left( {\bullet \rightarrow \bullet b}\right) \rightarrow a$ $\Rightarrow \left{ {\text{ from }\left( {3,W}\right) b \leq a \rightarrow b\text{ and }c\text{ transitive }}\right}$ $b \leq \left( {a \rightarrow b}\right) \rightarrow a$ $\left{ {\left( {{16},S}\right) }\right}$

(18) $\because a \rightarrow b \leq b \rightarrow a$

Similarly one derives from (17, C)

(19) $\bullet a \sim b \subseteq \cdot b \sim a$

Combining (19) with its instantiation $a,b \mathrel{\text{:=}} b,a$ yields (because of definition (2) of $\Rightarrow$ ) the important (20) $\because a \rightarrow b \approx b \rightarrow a$

it is important because it expresses that (but for equivalence) $a \rightarrow b$ is a symmetric

expression in $a,b\;$ .

Instanciating (19) with $b = a$ yields

(21) $\cdots a \subseteq a\;.\;$

Furthermore we observe

$\cdots \rightarrow b$ $\left{ \begin{array}{l} \left( {19}\right) \end{array}\right.$ with $a \mathrel{\text{:=}} \cdot a}$ [\left{ \begin{array}{l} \left( {18}\right) \text{ with }a,b \mathrel{\text{:=}} b,a \ a \rightarrow b \end{array}\right} ]

instantiating the above result with $b \mathrel{\text{:=}} \cdots a$ yields (again via (3,MP), (1) and reflexivity

$$ a \subseteq \dots a, $$

and in combination with (21)

(22) $a \approx a$

i.e. but for equivalence, $\bullet$ is its own inverse. We immediately use this result by observing for any $a,b$

$$ \begin{array}{l} a \rightarrow b \ = {(2 2) a n d (1 2) } \ \dots a \rightarrow b \ \equiv \left{ \begin{array}{l l} (1 9) \mathrm {w i t h} a := - a \end{array} \right} \ \cdot b \rightarrow \cdot a \ \end{array} $$

thus establishing

$a \rightarrow b \leq b \rightarrow a$

from which we conclude via (3,MP)

(23) $a \leq b \Rightarrow {b}^{ \land } \cdot a$

Combining finally (23) with its instantia. tion $a,b \mathrel{\text{:=}} b,a$ yields (with predicate calculus and definition (2) of $\Rightarrow$ )

(24) $a = b \Rightarrow a = b$

i.e. "preserves $\approx$ ",as we had set out to prove.

We now turn to section (iii) of our proof obligations, which asks us to show the existence of 3 operators that preserve $\simeq$ and enjoy further properties. The preservation of $\simeq$ by our new operators is a direct consequence of the fact that the latter are defined in terms of $\rightarrow$ and $\bullet$ , which -see(ii)- preserve $\simeq$ ; with this remark we consider the preservation of $\simeq$ by the new operators dealt with.

(iii, supremum) For any $a,b$ we define

(25) $a \uparrow b = a \sim b$

and shall prove that $\uparrow$ thus defined has the

desired property; on our way we shall prove a few things more.

But for equivalence, $\uparrow$ is symmetric. To demonstrate this, we observe for any $a,b$

(26) $a \uparrow b \approx b \uparrow a$

$$ \begin{array}{l} \equiv {(2 5) + \mathrm {t w i c e} } \ \cdot a \rightarrow b \simeq \cdot b \rightarrow a \ \equiv {2 0 } \ t r u e \ \end{array} $$

Moreover, $\uparrow$ is but for equivalence associative. To demonstrate this we observe for any $a,b,c$

$\left( {27}\right) \;a \uparrow \left( {b \uparrow c}\right) \simeq \left( {a \uparrow b}\right) \uparrow c$

$$ \begin{array}{l} \equiv \left{ \begin{array}{l} (2 6) + w i c e \end{array} \right} \ a \uparrow (c \uparrow b) \simeq c \uparrow (a \uparrow b) \ \equiv {2 5, \mathrm {f o u r t i m e s} } \ \cdot a \rightarrow (\cdot c \rightarrow b) \approx \cdot c \rightarrow (\cdot a \rightarrow b) \ = {(1 5, S) } \ t r u e \ \end{array} $$

That $a \uparrow b$ is an upper bound is expressed

$\left( {28}\right) \;a \leq a \uparrow b\;b \leq a \uparrow b$

it suffices to prove, say, the second conjunct, which we do by observing

$$ \begin{array}{r l}&b\\leq&{(3, w) }\&a \rightarrow b\=&{(2 5) }\&a \uparrow b\end{array} $$

which we immediately use to equate

$$ \begin{array}{r l} {(2 9)} & {b \approx a \uparrow b \equiv a \subseteq b} \ {\equiv} & {{(2) \mathrm {a n d} (2 8) }} \end{array} $$

(30) $a \uparrow b \leq b \equiv a \leq b\;\therefore$

after which we prove the latter by mutual implication

Proof We observe for $p = 2$

$$ \begin{array}{r l} & {\mathrm {a t} b \leq b} \ {\equiv} & {{(2 8) }} \ & {a \leq a \upharpoonright b \wedge a \upharpoonright b \leq b} \ {\Rightarrow} & {{\mathrm {f r a n s i t i v i} y \leq }} \ & {a \leq b.} \end{array} $$

We observe for

$$ \begin{array}{r l}&a \uparrow b \leq b\{\equiv}&{(2 5), (2 6) }\&b \rightarrow a \leq b\{\equiv}&{(2 2) }\&b \rightarrow a \leq b\end{array} $$

$$ \begin{array}{r l} {\Leftarrow} & {{(4 C) \mathrm {w i t h} a, b := b, a }} \ & {\cdot b \equiv a} \ {\Leftarrow} & {{(2 3) }} \end{array} $$

$$ a \le b $$

(End of Proof.)

And now we are ready to meet our final proof obligation for (iii, supremum)

(31) ${a}^{ \uparrow }b \leq c \equiv a \leq c \land b \leq c$

To this end we observe for any $a,b,c$

$$ a \uparrow b \leq c $$

$$ \begin{array}{l} \equiv {b \leq a + b \mathrm {a n d t r a n s i t i v i t y} \leq } \ a \upharpoonleft b \equiv c \land b \equiv c \ \equiv {2 9) t w i c e } \ c \simeq a \uparrow b \uparrow c \land c \simeq b \uparrow c \ \equiv \quad {\mathrm {L e i b n i z}: \uparrow \mathrm {a n d} \simeq \mathrm {p r e s e r v e} \simeq ! } \ c \simeq a ^ {\uparrow} c \wedge c \simeq b ^ {\uparrow} c \ \equiv \left{ \begin{array}{l l} (2 9) & \text {t w i c e} \end{array} \right} \ a \leq c \land b \leq c \ \end{array} $$

And this concludes our treatment of (iii, supremum).

(iii, infimum) After we define $\downarrow$ by

(32) $a \downarrow b = \left( {\cdot a \uparrow \cdot b}\right)$

• in which the reader is welcome to recognize a law of De Morgan-, our proof obligation

(33) $a \leq b \downarrow c \equiv a \leq b \wedge a \leq c$

is now a walk-over: we observe for any $a, b, c$

$$ \begin{array}{l} a \leq b \downarrow c \ \equiv {3 2 } \ a \equiv 0 (\cdot b \uparrow \cdot c) \ = {2 2) \& (2 3) } \ b \uparrow . c \leq a \ \equiv {3 1 } \ \cdot b \leq a \land \cdot a \leq a \ = {(2 2) \& (2 3) } \ a \leq b \land a \leq c \ \end{array} $$

And this concludes our treatment of (iii, infimum).

(iii, shunting) We define our unary operator by stating that for all $a$

$$ \sim a = \cdot a, \tag {34} $$

which turns our last proof obligation into

(35) $a \downarrow b \leq c \equiv b \equiv a \uparrow c$

Proof. We observe for any $a, b, c$

$$ \begin{array}{l} b \equiv a \uparrow c \ \equiv {2 5 } \& (2 6) } \ b \leq c \rightarrow a \ \equiv {(\mathbf {1 6}, S) } \ \therefore c \equiv b \rightarrow a \ \equiv \quad {(2 2) } \ \cdot c \equiv \dots b \rightarrow a \ \equiv {(\mathbf {2 5}) \& (\mathbf {2 6}) } \ \end{array} $$

$$ \cdot c \leq \cdot a \uparrow \cdot b $$

$$ \equiv {2 2) \& (2 3) } $$

$$ \cdot (a \uparrow b) \subseteq c $$

$$ \equiv {(\mathbf {3 2}) } $$

$$ a \downarrow b \equiv c $$

(End of Proof.)

Coda Rutger is not responsible for this text which was written by me (i.e. Edsger) in his absence. He is mentioned as co-author because he conceived the theorem and helped me out when I got stuck in my proof. effort. (That was in my effort to prove the Anti-Monotonicity.) He can explain better than I why he thought it worthwhile to design this theorem.

Nuenen, 22 July 1998

Rutger M. Dijkstra

Department of Computing Science

university of Groningen.

P.O.Box 300

9700 AV Groningen, The Netherlands e-Mail rutger@cs.rug.nl

prof. dPr Edsger W. Dgksfra

Department of Computer Sciences The University of Texas at Aust

Austin, TX 78712 - 1188 USA