Wednesday, October 5, 2011

EQ 11 Existential Quantification

(0) Notation ($$\vee$$ x | R : P ) $$\hspace{0.5 cm} \equiv \hspace{0.5 cm}$$ ($$\exists$$ x | R : P )

(1) Axiom: Generalized deMorgan: ($$\exists$$ x | R : P) $$\hspace{0.5 cm} \equiv \hspace{0.5 cm}$$ $$\neg$$( $$\forall$$ x | R : $$\neg$$ P)

(2) Theorem: Generalized deMorgan 1 : $$\neg$$ ($$\exists$$ x | R : $$\neg$$P) $$\hspace{0.5 cm} \equiv \hspace{0.5 cm}$$ ( $$\forall$$ x | R : P)

(3) Theorem: Generalized deMorgan 2 : $$\neg$$ ($$\exists$$ x | R : P) $$\hspace{0.5 cm} \equiv \hspace{0.5 cm}$$ ( $$\forall$$ x | R : $$\neg$$ P)

(4) Theorem: Generalized deMorgan 3 : ($$\exists$$ x | R : $$\neg$$ P) $$\hspace{0.5 cm} \equiv \hspace{0.5 cm}$$ $$\neg$$ ( $$\forall$$ x | R : P)

(5) Theorem: Trading 1: ($$\exists$$ x | R : P) $$\hspace{0.5 cm} \equiv \hspace{0.5 cm}$$ ( $$\exists$$ x | : R $$\wedge$$ P)

(6) Theorem: Trading 2: ($$\exists$$ x | S $$\wedge$$ R : P) $$\hspace{0.5 cm} \equiv \hspace{0.5 cm}$$ ( $$\exists$$ x | S : R $$\wedge$$ P)

(7) Theorem: Distributivity $$\frac{\wedge}{\exists}$$ ($$\exists$$ x | R : P) $$\wedge$$ Q $$\hspace{0.2 cm} \equiv \hspace{0.2 cm}$$ ($$\exists$$ x | R : P $$\wedge$$ Q)
not-occurs-free(x,Q)

(8) Theorem: ($$\exists$$ x | R : P) $$\hspace{0.2 cm} \equiv \hspace{0.2 cm}$$ ($$\exists$$ x |: R ) $$\wedge$$ P
not-occurs-free(x,P)

(9) Theorem: Distributivity $$\frac{\vee}{\exists}$$ ($$\exists$$x |:R) $$\Rightarrow$$ [($$\exists$$ x | R : P $$\vee$$ Q)] $$\hspace{0.2 cm} \equiv \hspace{0.2 cm}$$ ($$\exists$$ x | R : P) $$\vee$$ Q]
not-occurs-free(x,Q)

(10) Theorem: ($$\exists$$ x | R : false) $$\hspace{0.2 cm} \equiv \hspace{0.2 cm}$$ false

(11) Theorem: Range Weakening: ($$\exists$$ x | R : P) $$\hspace{0.2 cm} \equiv \hspace{0.2 cm}$$ ($$\exists$$ x | R $$\vee$$ S : P)

(12) Theorem: Body Weakening: ($$\exists$$ x | R : P) $$\hspace{0.2 cm} \equiv \hspace{0.2 cm}$$ ($$\exists$$ x | R : P $$\vee$$ Q)

(13) Theorem: Monotonicity of $$\exists$$
$$\exists$$ is monotonic in both body and range
(a) ($$\forall$$ x | R : A $$\Rightarrow$$ B ) $$\hspace{0.2 cm} \Rightarrow \hspace{0.2 cm}$$ [ ($$\exists$$ x | A : P) $$\Rightarrow$$ ($$\exists$$ x | B : P)]
(b) ($$\forall$$ x | R : A $$\Rightarrow$$ B ) $$\hspace{0.2 cm} \Rightarrow \hspace{0.2 cm}$$ [ ($$\exists$$ x | R : A) $$\Rightarrow$$ ($$\exists$$ x | R : B)]

(14) Theorem: P[ x := e] $$\hspace{0.2 cm} \Rightarrow \hspace{0.2 cm}$$ ($$\exists$$ x |: P)

(15) Theorem: Interchange of Quantifications
($$\exists$$ x | R ($$\forall$$ y | S : P)) $$\hspace{0.2 cm} \Rightarrow \hspace{0.2 cm}$$ ($$\forall$$ y | S ($$\exists$$ x | R : P))
not-occurs-free (x,S) $$\wedge$$ not-occurs-free(y, R)

Note: only when $$\exists$$ encloses $$\forall$$. The implication doesn't hold the other way.

(16) Meta Theorem Witness:
($$\exists$$ x | R : P) $$\Rightarrow$$ Q is a theorem $$\hspace{0.2 cm} \equiv \hspace{0.2 cm}$$ (R $$\wedge$$ P)[$$x$$ := $$\hat{x}$$] $$\Rightarrow$$ Q is a theorem,
not-occurs-free($$\hat{x}$$, [P,Q,R])
(a) often used when ($$\exists$$ x | R : P) is known and need to prove Q.
(b) with multiple statements, use distinct witnesses