Wednesday, October 5, 2011

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)

(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