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