Two cheers for equivalence

Two cheers for equivalence

Let us consider the operators $¬ , \vee$ , and $\equiv$ ; $¬$ is a unary operator, $\vee$ and $\equiv$ are symmetric and associative operators defined on bags of at least 2 operands. For the latter two we adopt the usual infix notation; the three operators have been listed in the order of decreasing syntactic binding power.

In the presence of $P \equiv R$ a new formula may be formed by replacing in an existing formula one or more occurrences of $P$ by $R$ . (Leibniz's Rule.)

Axiom 0 $P \equiv P \equiv Q \vee ¬ Q$

Parsing this $\left( {P \equiv P}\right) \equiv \left( {Q \vee ¬ Q}\right)$ we see that $Q \vee Q$ may be replaced by $P \equiv P$ ,which does not depend on $Q$ ! This suggests to introduce the abbreviation

${Ab} {br} 0$ $Q{v}_{7}Q \equiv {black}$

(where "black" may be viewed as a constant). Applying Leibniz's Rule to the above two formulas we generate

Theorem 0 $P \equiv P \equiv {black}$

Parsing this as $P \equiv \left( {P \equiv \text{black}}\right)$ ,and applying Leibniz's Rule we see that the suffix $\equiv$ black can be removed from a formula that ends on it; we are also free to add it to an existing formula. So we derive from Theorem O and Abbr.0 respectively

Theorem 1 $P \equiv P$

Theorem 2 $Q \vee \gamma Q$

We now add

Axiom 1 $P \vee {PQ} \equiv {PvQ} \equiv P$

Substituting $P$ for $Q$ in $Axiom 1$ yields

b l a c k \equiv P \vee P \equiv P

yielding with Theorem 0

Theorem 3 ${P}^{v}{P}^{ = }P$

Applying Theorem 3 to Abbr. O yields

Q \vee Q \vee ¬ Q \equiv b l a c k

yielding with Abbr. 0

Theorem 4 $P \vee {black} \equiv {black}$

Substituting black for $Q$ in ${Axiom}1$ yields

P v. I b l a c k \equiv P v. b l a c k \equiv P

and by application of Theorems 4 and O

Theorem 5. $P \vee \operatorname{black} \equiv P$

Substitution of $\tau$ black for $P$ in $A$ xiam 1 yields

[\text{black} \vee \text{TQ} \equiv \text{black} \vee \text{Q} \equiv \text{black}]

and by applying Theorem 5 twice we get

Theorem 6 ${7Q} \equiv Q \equiv 7$ black

Substitution of $¬ Q$ for $Q$ yields

7 7 Q \equiv 7 Q \equiv 7 b l a c k

and from the latter two we get with Leibniz's Rule

Theorem 7 ${77Q} \equiv Q$

Substituting in $A$ xiam 1 ${PvQ}$ for $Q$ ,we

[{P}{V!}\left( {{P}{V}Q}\right) \equiv {Pv}{P}_{V}Q \equiv P]

yielding with Theorem 3

P \vee ¬ (P \vee Q) \equiv P \vee Q \equiv P

Confronting this with Axiom 1, we get

Theorem 8 $P \vee ¬ \left( {{P}_{v}Q}\right) \equiv {Pv} ∧ Q$

Substituting $P \equiv Q$ for $Q$ in Theorem 6 we get

\lnot (P \equiv Q) \equiv P \equiv Q \equiv \lnot b l a c k

and applying Theorem 6 once more we generate

Theorem 9 $¬ \left( {P \equiv Q}\right) \equiv P \equiv ¬ Q$

With Theorems 1 and 6 we generate in suc-

cession

\lnot b l a c k \equiv \lnot b l a c k \equiv b l a c k

P \equiv ¬ P \equiv R \equiv ¬ R \equiv Q \equiv ¬ Q, i.e.

Theorem 10 $P \equiv Q \equiv R \equiv 7P \equiv Q \equiv 7R$

Substitution of ${IP}$ for $P$ in $A$ xiam 1 yields

\lnot P \lor \lnot Q \equiv \lnot P \lor Q \equiv \lnot P

With Theorem 10 this yields

\lnot (\lnot P \lor \lnot Q) \equiv \lnot P \lor Q \equiv P

and with

Abbr.1 $¬ \left( {¬ P \vee ¬ Q}\right) \equiv P ∧ Q$

Theorem 11. $P ∧ Q \equiv 7{P}_{V}Q \equiv P$

In the sequel, appeals to Abbr.1 and Theorem 7 wil often be summarized by referring to the law of de Morgan.

Substitution of $P ∧ Q$ for $Q$ in Axiom 1 yields

P _ {V} (P ∧ Q) \equiv P \lor (P ∧ Q) \equiv P

With de Morgan's Law

P \vee ¬ P \vee ¬ Q \equiv P \vee (P \wedge Q) \equiv P

With Abbr.0 , Theorems 4 and O we generate

Theorem 12 $P \vee \left( {P ∧ Q}\right) \equiv P$

Interchanging in Axiom 1 $P$ and $Q$ gives

Q \vee ¬ P \equiv P \vee Q \equiv Q

which yields with Axiom 1

\mathrm {T h e o r e m 1 3} P \equiv Q \equiv Q v _ {7} P \equiv P v _ {7} Q

Applying Theorem 12 we derive from Theorem 13

P \equiv Q \equiv Q \vee (Q \wedge ¬ P) \vee ¬ P \equiv P \vee ¬ Q

with de Morgan's Law

P \equiv Q \equiv ¬ (P v ¬ Q) v (Q v ¬ P) \equiv P v ¬ Q

and applying Theorem 11, we generate

\mathrm {T h e o r e m 1 4} P \equiv Q \equiv (P v _ {1} Q) \wedge (Q v _ {1} P)

Note Theorem 14 corresponds to the Hilbert-Rockermann definition of equivalence. (End of Note.)

From Theorem 4 we derive

Q vR v black

from which we generate with Abbr. 0

QvP v RvP

which yields with Theorem 8 (twice)

Q \vee ¬ (Q \vee ¬ P) \vee R \vee ¬ (R \vee P)

which yields with de Morgan's Law

\mathrm {T h e o r e m 1 5} (¬ Q ∧ P) \lor (¬ R ∧ ¬ P) \lor Q \lor R

Note Theorem 15 corresponds to the last axiom of Hilbert. Ackermann

(P ⇒ Q) ⇒ ((P \vee R) ⇒ (Q \vee R))

(End of Note)

Now comes a trivial section that I shall only indicate. With

Abbr. 2 black = white

we leave it to the reader to generate - mostly with de Morgan's law- all sorts of useful theorems such as

\begin{array}{l} Q ∧ Q \equiv w h i t e \ P ∧ P \equiv P \ P \wedge w h i t e \equiv w h i t e \ P ∧ b l a c k \equiv P \ P ∧ (P \lor Q) \equiv P ∧ Q \ P ∧ (P \lor Q) \equiv P \ \end{array}

So far I did not succeed in generating, say

(P \equiv Q) \wedge (P \equiv R) \equiv (P \equiv Q) \wedge (Q \equiv R)

or the distributivity of $∧$ and $\lor$ . I have tried whether I could modify my axioms - currently, none of them contains three variables - but did not succeed. The obvious alternative is the generalization of Leibniz's Rule: if $Q$ could be generated in the additional presence of $P$ , we allow ourselves to generate

Since I don't want to become a logician I had better stop ; in any case I have had my fun.

Plataansstraat 5 5671 AL NUENEN The Netherlands

24 October 1982 prop. dr. Edsger W. Dgkstra Burroughs Research Fellow