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