EQ 10 Universal Quantification

(0) Notation: (\(\wedge\) x | R : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x | R : P)

(1) Axiom: Trading: (\(\forall\) x | R : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x |: R \(\Rightarrow\) P)

Trading Theorems

(2) Theorem (\(\forall\) x | R : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x |: \(\neg\)R \(\vee\) P)

(3)Theorem (\(\forall\) x | R : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x |: R \(\vee\) P \(\equiv\) P)

(4)Theorem (\(\forall\) x | R : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x |: R \(\wedge\) P \(\equiv\) R)

(5) Theorem (\(\forall\) x | R \(\wedge\) S : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x | S : R \(\Rightarrow\) P)

(6) Theorem (\(\forall\) x | R \(\wedge\) S : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x | S : \(\neg\)R \(\vee\) P)

(7)Theorem (\(\forall\) x | R \(\wedge\) S : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x | S : R \(\vee\) P \(\equiv\) P)

(8)Theorem (\(\forall\) x | R \(\wedge\) S: P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x | S : R \(\wedge\) P \(\equiv\) R)

(9) Axiom: Distributivity \(\frac{\vee}{\forall}\) Q \(\vee\) (\(\forall\) x | R : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x | R : P \(\vee\) Q)
not-occurs-free(x,Q)

(10)Theorem: (\(\forall\) x | R :P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\forall\) x |: \( \neg \)R) \(\vee\) P
not-occurs-free(x,P)

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

Be careful using this theorem. A conjunct can be moved outside the scope of the quantification only if the Range is not everywhere false

(12) Theorem: (\( \forall \) x | R : true) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) true

(13) Theorem: (\( \forall \) x | R : P \(\equiv\) Q) \(\hspace{0.2 cm} \Rightarrow \hspace{0.2 cm}\) [(\( \forall \) x | R : P ) \(\Rightarrow\) (\( \forall \) x | R : Q ) ]

(14) Theorem: Range Weakening/Strengthening (\( \forall \) x | R \(\vee\) S : P ) \(\hspace{0.2 cm} \Rightarrow \hspace{0.2 cm}\) (\( \forall \) x | R : P )

(15) Theorem: Body Weakening/Strengthening (\( \forall \) x | R : P \(\wedge\) Q ) \(\hspace{0.2 cm} \Rightarrow \hspace{0.2 cm}\) (\( \forall \) x | R : P )

(16) Theorem: Monotonicity of \(\forall\):
(a) \(\forall\) is antimonotonic in its range: (\(\forall\) x | R : A \(\Rightarrow\) B ) \(\hspace{0.2 cm} \Rightarrow \hspace{0.2 cm}\) [(\(\forall\) x | A : P ) \(\Leftarrow\) (\(\forall\) x | B : P)]
(b) \(\forall\) is monotonic in its body: (\(\forall\) x | R : A \(\Rightarrow\) B ) \(\hspace{0.2 cm} \Rightarrow \hspace{0.2 cm}\) [(\(\forall\) x | R : A ) \(\Rightarrow\) (\(\forall\) x | R : B)]

(17) Instantiation (\( \forall \) x |: P) \(\hspace{0.2 cm} \Rightarrow \hspace{0.2 cm}\) P [x := e]

(18) MetaTheorem: P is a theorem \( \equiv \) (\(\forall\) x |: P) is a theorem