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