HOME

Some useful formulae

Show original manuscript

Let f be a propositional expression and R a propositional variable. Using the slash "/" to denote "substituted for", we have the general equivalences

f ≡ ( f ( false / R ) ∨ R ) ∧ ( f ( true / R ) ∨ ¬ R )

f ≡ ( f ( true / R ) ∧ R ) ∨ ( f ( false / R ) ∧ ¬ R ) .

(We don't prove this; it should probably be proved using induction over the syntax.)

The purpose of this note is to draw the attention to a few special instances.

PQR ≡ (( PQ ) ∨ R ) ∧ ( P ∨ ¬ R )

PQR ≡ (¬ PR ) ∧ (( PQ ) ∨ ¬ R ) .

(Substituting in the latter formula ¬P for P we get

PQR ≡ ( PR ) ∧ (( PQ ) ∨ ¬ R ) .

We used the last formula recently to prove

( yza ) ∧ ( zyb ) ≡

( ya ) ∧ ( zb ) ∧ (( yz ) ∨ ¬ ( ab )) .)

Plataanstraat 5
5671 AL NUENEN
The Netherlands
8 February 1984
drs. A.J.M. van Gasteren
prof.dr. Edsger W. Dijkstra