959

A short note on universal quantification

EWD959 · 1984–1987 · PDF · Source language: English. · Local OCR-derived source needs manual review.

A short note on universal quantification

With the dummy $x$ ranging over some anonymous range and using

(0) $\left\lbrack {\left( {{\underline{\pi }}{1} : {p}{1}x}\right) \land \left( {{\underline{\pi }}{2} : {q}{2}x}\right) \equiv \left( {{\underline{\pi }}{1} : {p}{1}x \land {q}_{1}x}\right) }\right\rbrack$

we shall show

(1) $\left\lbrack {\left( {{\underline{\pi }}{X} : p.x \equiv q.x}\right) \Rightarrow \left( {\left( {{\underline{\pi }}{X} : p.x}\right) \equiv \left( {{\underline{\pi }}_{X} : q.x}\right) }\right) }\right\rbrack$ (2) $\left\lbrack {\left( {\underline{A}x}\right) \cdot p.x \Rightarrow q.x}\right) \Rightarrow \left( {\left( {\underline{A}x}\right) \cdot p.x}\right) \Rightarrow \left( {\underline{A}x}\right) \cdot \left( {q.x}\right) )\rbrack$

from propositional calculus we shall use

(3) $\left\lbrack {X \Rightarrow \left( {P \equiv Q}\right) \equiv X \land P \equiv X \land Q}\right\rbrack$ (4) $\left\lbrack {\left( {P \equiv Q}\right) \land P \equiv P \land Q}\right\rbrack$

$$ \begin{array}{l} \mathrm {P r o o f} _ {\mathrm {o f}} (3) \quad X \Rightarrow (P \equiv Q) \ = \left{ \begin{array}{l l} p r e d. c a l c \end{array} \right} \ = {\mathrm {d i s t r i b u t i o n} } \ i X \vee i P \equiv i X \vee i Q \ = {d e M o r g a n } \ X \wedge P = X \wedge Q \ \end{array} $$

(End of Proof)

$$ \begin{array}{l} \mathrm {P r o o f} _ {\mathrm {o f}} (4) \quad (P \equiv Q) \land P \ = {p, c, } \ (\overrightarrow {P} \neq Q) \land P \ = {\mathrm {d i s t r i b u l i o n} } \ i P \land P \ne Q \land P \ = {p, c, } \ P \land Q \ \end{array} $$

(End of Proof.)

Proof of (1) Denoting for brevity's sake universal quantification over $x$ by "II". We observe

$$ \begin{array}{l} \left[ [ p \equiv q ] \right] \Rightarrow (\left[ [ p ] \right] = \left[ [ q ] \right]) \ = {(3) } \ | [ p \equiv q ] | \wedge | [ p ] | \equiv | [ p \equiv q ] | \wedge | [ q ] | \ = {0) t w i c e } \ | [ (p \equiv q) \wedge p ] | \equiv | [ (p \equiv q) \wedge q ] | \ = {(4) \mathrm {t w i c e} } \ | [ p \wedge q ] | = | [ q \wedge p ] | \ = {p c } \ \mathbf {f r u e} \ \end{array} $$

(End of Proof)

Proof of (2) With the same notational convention

$$ \begin{array}{l} [ p \Rightarrow q ] ] \ = {p < } \ \left| \left[ p \wedge q \equiv p \right] \right| \ \Rightarrow \quad {(1) } \ | [ p \wedge q ] | = | [ p ] | \ = {(0) } \ | [ p ] | \wedge | [ q ] | \equiv | [ p ] | \ = {p, c } \ \left| \left[ p \right] \right| \Rightarrow \left| \left[ q \right] \right| \ \end{array} $$

(End of Proof.)

With thanks to C.S. Scholle

Austin 20 May 1986

pror. dr. Edsger W. Dyksstra

Department of Computer Sciences

The University of Texas at Austin

Austin, TX. 78712-1188

United States of America.