(1) Monoids And Abelian Monoids
Binary Operator \( \star \) is associative and has an identity \( \equiv \) it is a monoid. If it is also symmetric, it is an abelian monoid.
In the following the \( \star \) represents an operator that is an abelian monoid. All theorems don't strictly need the "abelian-ness", but the operators we deal with are all abelian, so the assumption does no harm.
(2) General Form of Quantification
( \( \star \) x:type1, y:type2 ..) | Range:\( \mathcal{B} \) : Predicate:type3)
x,y,... are bound variables or 'dummmies'
the Predicate is also known as the "body".
(3) Definition of 'free'
(a) The *occurrence* of i, in an expression i is free
(b) If an occurrence of a variable i in expression E is free, then so is the occurrence in (E), function application arguments f(....E...) [note: binary operators are considered function applications)[, (\( \star \)x|E:P) and (\( \star \)x|R:E) (as long as i is not one of the variables in the dummy list x.)
(4) Definition of 'bound'
(a) If an occurrence of a variable i in expression E is free, then that occurrence is bound to dummy i in (\( \star \)x|E:P) and ( \(\star \)x|R:E) if i occurs in dummy list x.
(b) If an occurrence of i is bound in expression E, then it is also bound to the same dummy in (E), function application arguments f(....E...) [note: binary operators are considered function applications)], (\( \star \)x|E:P) and (\( \star \)x|R:E)
(5) Definition of occurs-free and not-occurs-free
occurs-free(v,e) is defined to mean that at least one variable from the list-of-variables v occurs free in at least one expression in list of expressions v
not-occurs-free(v,e) \( \equiv \) \( \neg \)occurs-free(v,e) \( \equiv \) no variable in list-of-variables v occurs free in any of the expressions in list-of-expressions e
(6) Textual Substitution
Extending textual substitution to quantified statements
( \(\star\) x | R : P)[y := F] \( \hspace{0.2 cm}\equiv\hspace{0.2 cm} \) \( (\star\) x | R[y := F] : P[y := F]),
given not-occurs-free(x,[y,F])), iow none of the bound variables is free on either side of the := . If a bound variable does occur free on either side of :=, replace *the bound variable* with a fresh variable j. This ensures that a free variable in the textual substitution y := F does not become bound.
Extending Leibniz inference rule to handle substitution of either side of an equality into a quantified statement
(7) Leibniz 1
\( \frac{A\hspace{0.2 cm}=\hspace{0.2 cm}B}{(\star x |R [z:=A]: P ) \hspace{0.2 cm}=\hspace{0.2 cm} (\star x |R [z:=B]: P )} \)
(8) Leibniz 2
\( \frac{R\hspace{0.2 cm}\Rightarrow\hspace{0.2 cm}A\hspace{0.2 cm}=\hspace{0.2 cm}B}{(\star x |R : P[z:=A] ) \hspace{0.2 cm}=\hspace{0.2 cm} (\star x |R : P [z:=B])} \)
(9) Axiom: Empty Range: ( \(\star\) x | false : P ) \(\hspace{0.2 cm} \equiv\hspace{0.2 cm} \) u (the identity of \( \star \))
(10) Axiom: One Point Range: ( \(\star\) x | x = E : P ) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) P[ x := E ]
provided not-occurs-free (x,E)
(11) Axiom: Distributivity: ( \(\star\) x | R : P ) \(\star\) ( \(\star\) x | R : Q ) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) ( \(\star\) x | R : P \(\star\) Q )
provided each quantification is defined (quantifications with finite ranges are always defined as are quantifications with \(\star\) being either \(\wedge\) or \(\vee\). if \(\star\) is +, then you have to check for convergence of the summation, etc)
(12) Axiom: Range Split 1: ( \(\star\) x | R \(\vee\) S: P ) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) ( \(\star\) x | R : P ) \(\star\) ( \(\star\) x | S : P )
provided (R \(\wedge\) S) is false \(\wedge\) each quantification is defined
(13) Axiom: Range Split 2: ( \(\star\) x | R \(\vee\) S: P ) \( \star\) ( \(\star\) x | R \(\wedge\) S: P ) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) ( \(\star\) x | R : P ) \(\star\) ( \(\star\) x | S : P )
provided each quantification is defined
(14) Axiom: Range Split 3: ( \(\star\) x | R \(\vee\) S: P ) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) ( \(\star\) x | R : P ) \(\star\) ( \(\star\) x | S : P )
provided \(\star\) is idempotent \(\wedge\) each quantification is defined
Note: Definition of idempotent: \(\star\) is idempotent \( \equiv\) ( a \(\star\) a \(\equiv\) a)
(15) Axiom: Interchange of Dummies: ( \(\star\) x | R :( \(\star\) y | S : P) ) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) ( \(\star\) y | S :( \(\star\) x| R : P) )
provided not-occurs-free(x,S) \(\wedge\) not-occurs-free(y,R) \(\wedge\) each quantification is defined
iow "nested quantifications with the same operator can be interchanged"
(16) Axiom: Dummy Nesting: (\(\star\) x,y | R \(\wedge\) S : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) ( \(\star\) x | R :( \(\star\) y | S : P) )
provided not-occurs-free(y,R)
iow " a single quantification over a list of dummies can be viewed as nested quantification"
(17) Axiom: Dummy Renaming: (\(\star\)x | R : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\star\)y | R[x := y] : P[x := y])
provided not-occurs-free (y, [R,P])
iow "one dummy can be replaced consistently by another dummy"
(18) Theorem: Change of Dummy (Generalization of Dummy Renaming) (\(\star\)x | R : P) \(\hspace{0.2 cm} \equiv \hspace{0.2 cm}\) (\(\star\)x | R [x := f.y] : P[x := f.y])
provided not-occurs-free (y,[R,P]) \(\wedge\) f is an invertible function such that x = \(f.y\) and y = \(f^{-1}.x\)
Example: Consider (+ \(i\) | 2 \(\leq\) \(i\) \(\leq\) 10 : \(i^2\) ) and we need to have a range starting with zero
the reqd range is (2 - 0) \(\leq\) \(i - 2 \) \(\leq\) (10 - 2)
let k = (i - 2) this is new dummy expressed in terms of old = \(f^{-1}.i\) = k = i - 2
so i = k + 2 this is old dummy expressed in terms of new = \(f.k\) = i = k + 2
\(\hspace{2 cm}\)(+ \(i\) | 2 \(\leq\) \(i\) \(\leq\) 10 : \(i^2\) )
= \(\hspace{0.5 cm}\) Dummy Renaming Theorem. Rename the dummy from i to k with i = f.k = k - 2
\(\hspace{2 cm}\)(+ \(k\) | 2 \(\leq\) \(k+2\) \(\leq\) 10 : \((k+2)^2\) )
= \(\hspace{0.5 cm}\) arithmetic a \(\leq\) b \(\leq\) c \( \equiv \) a-2 \(\leq\) b-2 \(\leq\) c-2
\(\hspace{2 cm}\)(+ \(k\) | 0 \(\leq\) \(k\) \(\leq\) 8 : \((k+2)^2\) )
(19) Theorem: Split off term 1
(\(\star i\) | \(0 \leq i \lt n+1\) : P) \( \equiv \) (\(\star i\) | \(0 \leq i \lt n\) : P) \(\star\) P[i := n ]
(20) Theorem: Split off term 2
(\(\star i\) | \(0 \leq i \lt n+1\) : P) \( \equiv \) P[i := 0 ] \(\star\) (\(\star i\) | \(0 \lt i \lt n + 1\) : P)
Wednesday, October 5, 2011
Tuesday, October 4, 2011
EQ 8 Proof By Induction
(1) Axiom: Mathematical Induction Over \( \mathcal{N} \). Form 1
( \( \forall \) n:\( \mathcal{N} \) |: ( \( \forall \)i | 0 \( \leq \) i \( \lt \) n: \(P_i\)) \( \Rightarrow \) \(P_n\) ) \( \Rightarrow\) ( \( \forall \) n : \( \mathcal{N} \) : \(P_n\))
used to prove Universal Quantification By Induction
(2) Theorem: Mathematical Induction Over \( \mathcal{N} \). Form 2
( \( \forall \) n:\( \mathcal{N} \) |: ( \( \forall \)i | 0 \( \leq \) i \( \lt \) n: \(P_i\)) \( \Rightarrow \) \(P_n\) ) \( \equiv\) ( \( \forall \) n : \( \mathcal{N} \) : \(P_n\))
used to prove properties of Induction
(3) Theorem: Mathematical Induction Over \( \mathcal{N} \). Form 3
\( P_0\) \( \wedge \) ( \( \forall \) n:\( \mathcal{N} \) |: ( \( \forall \)i | 0 \( \leq \) i \( \leq \) n: \( P_i\) ) \( \Rightarrow \) \( P_{n+1} \) ) \( \Rightarrow\) ( \( \forall \) n : \( \mathcal{N} \) : \(P_n\))
restatement of (1) used for inductive proofs
(4) Parts of Mathematical Induction axiom
\( P_0\) is the base case
( \( \forall \) n:\( \mathcal{N} \) |: ( \( \forall \)i | 0 \( \leq \) i \( \leq \) n: \( P_i\) ) \( \Rightarrow \) \( P_{n+1} \) ) \( \Rightarrow\) ( \( \forall \) n : \( \mathcal{N} \) : \(P_n\)) is the inductive case
( \( \forall \) n:\( \mathcal{N} \) |: ( \( \forall \)i | 0 \( \leq \) i \( \leq \) n: \( P_i\) ) \( \Rightarrow \) \( P_{n+1} \) ) is the inductive hypothesis
(5) Normal Proof Method
(1) Prove Base Case. \( P_0 \)
(2) Assume arbitrary n \( \ge \) 0
(3) Assume Inductive Case ( \( \forall \)i | 0 \( \leq \) i \( \leq \) n: \( P_i\) )
(4) Prove \( P_{n+1} \)
(6) Induction starting at other integers
Let a sequence of integers start at \( n_0 \) Then Inductive Theorem is
\( P_{n_0}\) \( \wedge \) ( \( \forall \) n:\(n_0 \leq n \)|: ( \( \forall \)i | \(n_0 \leq \) i \( \leq \) n: \( P_i\) ) \( \Rightarrow \) \( P_{n+1} \) ) \( \Rightarrow\) ( \( \forall \) n : \(n_0 \leq n \) : \(P_n\))
( \( \forall \) n:\( \mathcal{N} \) |: ( \( \forall \)i | 0 \( \leq \) i \( \lt \) n: \(P_i\)) \( \Rightarrow \) \(P_n\) ) \( \Rightarrow\) ( \( \forall \) n : \( \mathcal{N} \) : \(P_n\))
used to prove Universal Quantification By Induction
(2) Theorem: Mathematical Induction Over \( \mathcal{N} \). Form 2
( \( \forall \) n:\( \mathcal{N} \) |: ( \( \forall \)i | 0 \( \leq \) i \( \lt \) n: \(P_i\)) \( \Rightarrow \) \(P_n\) ) \( \equiv\) ( \( \forall \) n : \( \mathcal{N} \) : \(P_n\))
used to prove properties of Induction
(3) Theorem: Mathematical Induction Over \( \mathcal{N} \). Form 3
\( P_0\) \( \wedge \) ( \( \forall \) n:\( \mathcal{N} \) |: ( \( \forall \)i | 0 \( \leq \) i \( \leq \) n: \( P_i\) ) \( \Rightarrow \) \( P_{n+1} \) ) \( \Rightarrow\) ( \( \forall \) n : \( \mathcal{N} \) : \(P_n\))
restatement of (1) used for inductive proofs
(4) Parts of Mathematical Induction axiom
\( P_0\) is the base case
( \( \forall \) n:\( \mathcal{N} \) |: ( \( \forall \)i | 0 \( \leq \) i \( \leq \) n: \( P_i\) ) \( \Rightarrow \) \( P_{n+1} \) ) \( \Rightarrow\) ( \( \forall \) n : \( \mathcal{N} \) : \(P_n\)) is the inductive case
( \( \forall \) n:\( \mathcal{N} \) |: ( \( \forall \)i | 0 \( \leq \) i \( \leq \) n: \( P_i\) ) \( \Rightarrow \) \( P_{n+1} \) ) is the inductive hypothesis
(5) Normal Proof Method
(1) Prove Base Case. \( P_0 \)
(2) Assume arbitrary n \( \ge \) 0
(3) Assume Inductive Case ( \( \forall \)i | 0 \( \leq \) i \( \leq \) n: \( P_i\) )
(4) Prove \( P_{n+1} \)
(6) Induction starting at other integers
Let a sequence of integers start at \( n_0 \) Then Inductive Theorem is
\( P_{n_0}\) \( \wedge \) ( \( \forall \) n:\(n_0 \leq n \)|: ( \( \forall \)i | \(n_0 \leq \) i \( \leq \) n: \( P_i\) ) \( \Rightarrow \) \( P_{n+1} \) ) \( \Rightarrow\) ( \( \forall \) n : \(n_0 \leq n \) : \(P_n\))
EQ 7: Leibniz Axiom and Theorems
(1) Axiom, Leibniz: (e = f) \( \Rightarrow \) \( E_e^z = E_f^z \)
Note 1: difference between Leibniz Inference Rule and the Leibniz Axiom.
The inference rule states that if X = Y in all states then \( E_X^z = E_Y^z\) in all states.
The axiom states that if (x = y) in one state then \(E_x^z = E_y^z \) in that state.
Note 2: the implication is one way. iow \( E_e^z = E_f^z \) \( \nRightarrow \) (e = f)
e.g: Let E \( \equiv \) false \( \wedge \) zee . Here \( E_e^z = E_f^z \) but e \( \neq \) f
Substitution Theorems:
If an equality conjuncts or implies, or a conjunction with an equality as a conjunct implies , an Expression E containing one side of the equality, you can replace that part of E with the other side of the equality.
(2) Theorem: Substitution 1: (e = f) \( \wedge\) \( E_e^z \equiv \) (e = f) \( \wedge\) \( E_f^z \)
(3) Theorem: Substitution 2: (e = f) \( \Rightarrow\) \( E_e^z \equiv \) (e = f) \( \Rightarrow\) \( E_f^z \)
(4) Theorem: Substitution 3: q \( \wedge \) (e = f) \( \Rightarrow\) \( E_e^z \equiv \) q \( \wedge \) (e = f) \( \Rightarrow\) \( E_f^z \)
Replace By True Theorems:
If a variable conjuncts or implies, or a conjunction with a variable as a conjunct implies an expression E containing that variable, the occurences of the variable in the expression can be replaced by true
(5) Theorem Replace by true 1: p \( \wedge\) \( E_p^z \equiv \) p \( \wedge\) \( E_{true}^z \)
(6) Theorem: Replace by true 2: p \( \Rightarrow \) \( E_p^z \equiv \) p \( \Rightarrow \) \( E_{true}^z \)
(7) Theorem: Replace by true 3: q \( \wedge \) p \( \Rightarrow \) \( E_p^z \equiv \) q \( \wedge \) p \( \Rightarrow \) \( E_{true}^z \)
Example:
Prove p \( \wedge \) q \( \Rightarrow \) ( p \( \equiv \) q)
\( \hspace{2 cm }\) p \( \wedge \) q \( \Rightarrow \) ( p \( \equiv \) q)
=\( \hspace{0.5 cm } \) recognize pattern. conjunction with a variable (p) on one side implying an expression containing the same variable
\( \hspace{0.5 cm } \) invoke Theorem (6) above, replace p in expression by true
\( \hspace{2 cm }\) p \( \wedge \) q \( \Rightarrow \) ( true \( \equiv \) q)
=\( \hspace{0.5 cm } \) recognize pattern. conjunction with a variable (q) on one side implying an expression containing the same variable
\( \hspace{0.5 cm } \) invoke Theorem (6) above, replace q in expression by true
\( \hspace{2 cm }\) p \( \wedge \) q \( \Rightarrow \) ( true \( \equiv \) true)
=\( \hspace{0.5 cm } \) Theorem: true is the identity of \( \equiv \), m \( \equiv \) m \( \equiv \) true
\( \hspace{2 cm }\) p \( \wedge \) q \( \Rightarrow \) true
=\( \hspace{0.5 cm } \) Theorem: true is the Right Zero of \( \Rightarrow \), m \( \Rightarrow \) true \( \equiv \) true
\( \hspace{2 cm }\) true
Replace By False Theorems:
If an Expression E containing a variable p disjuncts p, implies p or implies a disjunction with p on one side,p can be replaced by false in the expression
(8) Theorem: Replace by False 1: \( E_p^z\) \( \vee \) p \( \equiv \) \( E_{false}^z\) \( \vee \) p
(9) Theorem: Replace by False 2: \( E_p^z\) \( \Rightarrow \) p \( \equiv \) \( E_{false}^z\) \( \Rightarrow \) p
(10) Theorem: Replace by False 2: \( E_p^z\) \( \Rightarrow \) p \(\vee\) q \( \equiv \) \( E_{false}^z\) \( \Rightarrow \) p \(\vee\) q
(11) Theorem: Shannon: \( E_p^z\) \( \equiv \) ( p \(\wedge\) \( E_{true}^z\) ) \(\vee\) ( \( \neg \) p \(\wedge\) \( E_{false}^z\) )
Note 1: difference between Leibniz Inference Rule and the Leibniz Axiom.
The inference rule states that if X = Y in all states then \( E_X^z = E_Y^z\) in all states.
The axiom states that if (x = y) in one state then \(E_x^z = E_y^z \) in that state.
Note 2: the implication is one way. iow \( E_e^z = E_f^z \) \( \nRightarrow \) (e = f)
e.g: Let E \( \equiv \) false \( \wedge \) zee . Here \( E_e^z = E_f^z \) but e \( \neq \) f
Substitution Theorems:
If an equality conjuncts or implies, or a conjunction with an equality as a conjunct implies , an Expression E containing one side of the equality, you can replace that part of E with the other side of the equality.
(2) Theorem: Substitution 1: (e = f) \( \wedge\) \( E_e^z \equiv \) (e = f) \( \wedge\) \( E_f^z \)
(3) Theorem: Substitution 2: (e = f) \( \Rightarrow\) \( E_e^z \equiv \) (e = f) \( \Rightarrow\) \( E_f^z \)
(4) Theorem: Substitution 3: q \( \wedge \) (e = f) \( \Rightarrow\) \( E_e^z \equiv \) q \( \wedge \) (e = f) \( \Rightarrow\) \( E_f^z \)
Replace By True Theorems:
If a variable conjuncts or implies, or a conjunction with a variable as a conjunct implies an expression E containing that variable, the occurences of the variable in the expression can be replaced by true
(5) Theorem Replace by true 1: p \( \wedge\) \( E_p^z \equiv \) p \( \wedge\) \( E_{true}^z \)
(6) Theorem: Replace by true 2: p \( \Rightarrow \) \( E_p^z \equiv \) p \( \Rightarrow \) \( E_{true}^z \)
(7) Theorem: Replace by true 3: q \( \wedge \) p \( \Rightarrow \) \( E_p^z \equiv \) q \( \wedge \) p \( \Rightarrow \) \( E_{true}^z \)
Example:
Prove p \( \wedge \) q \( \Rightarrow \) ( p \( \equiv \) q)
\( \hspace{2 cm }\) p \( \wedge \) q \( \Rightarrow \) ( p \( \equiv \) q)
=\( \hspace{0.5 cm } \) recognize pattern. conjunction with a variable (p) on one side implying an expression containing the same variable
\( \hspace{0.5 cm } \) invoke Theorem (6) above, replace p in expression by true
\( \hspace{2 cm }\) p \( \wedge \) q \( \Rightarrow \) ( true \( \equiv \) q)
=\( \hspace{0.5 cm } \) recognize pattern. conjunction with a variable (q) on one side implying an expression containing the same variable
\( \hspace{0.5 cm } \) invoke Theorem (6) above, replace q in expression by true
\( \hspace{2 cm }\) p \( \wedge \) q \( \Rightarrow \) ( true \( \equiv \) true)
=\( \hspace{0.5 cm } \) Theorem: true is the identity of \( \equiv \), m \( \equiv \) m \( \equiv \) true
\( \hspace{2 cm }\) p \( \wedge \) q \( \Rightarrow \) true
=\( \hspace{0.5 cm } \) Theorem: true is the Right Zero of \( \Rightarrow \), m \( \Rightarrow \) true \( \equiv \) true
\( \hspace{2 cm }\) true
Replace By False Theorems:
If an Expression E containing a variable p disjuncts p, implies p or implies a disjunction with p on one side,p can be replaced by false in the expression
(8) Theorem: Replace by False 1: \( E_p^z\) \( \vee \) p \( \equiv \) \( E_{false}^z\) \( \vee \) p
(9) Theorem: Replace by False 2: \( E_p^z\) \( \Rightarrow \) p \( \equiv \) \( E_{false}^z\) \( \Rightarrow \) p
(10) Theorem: Replace by False 2: \( E_p^z\) \( \Rightarrow \) p \(\vee\) q \( \equiv \) \( E_{false}^z\) \( \Rightarrow \) p \(\vee\) q
(11) Theorem: Shannon: \( E_p^z\) \( \equiv \) ( p \(\wedge\) \( E_{true}^z\) ) \(\vee\) ( \( \neg \) p \(\wedge\) \( E_{false}^z\) )
Sunday, October 2, 2011
EQ 6: Monotonicity
(a) Definition.
A function f is monotonic in its argument \( \equiv \) (x \( \Rightarrow \) y) \( \hspace{0.2 cm } \Rightarrow \hspace{0.2 cm } \) (f.x \( \Rightarrow \) f.y)
Note: The textual substitution approach in the Inference Rules provided below are a better way to work out monotonicity etc than a 'function' approach using above idea.
A function is anti-monotonic in its argument \( \equiv \) (x \( \Rightarrow \) y) \( \hspace{0.2 cm } \Rightarrow \hspace{0.2 cm } \) (f.x \( \Leftarrow \) f.y)
(b) Monotonicity of Logical Operators
\( \hspace{0.5 cm } \vee \) Monotonic. (p \( \Rightarrow \) q) \( \hspace{0.2 cm } \Rightarrow \hspace{0.2 cm } \) (p \( \vee \) r) \( \Rightarrow \) (q \( \vee \) r )
\( \hspace{0.5 cm } \wedge \) Monotonic. (p \( \Rightarrow \) q) \( \hspace{0.2 cm } \Rightarrow \hspace{0.2 cm } \) (p \( \wedge \) r) \( \Rightarrow \) (q \( \wedge \) r )
\( \hspace{0.5 cm } \neg \) Antimonotonic. (p \( \Rightarrow \) q) \( \hspace{0.2 cm } \Rightarrow \hspace{0.2 cm } \) ( \( \neg \) p \( \Leftarrow \) \( \neg \) q )
\( \hspace{0.5 cm } \Rightarrow \) Antimonotonic Antecedent. (p \( \Rightarrow \) q) \( \hspace{0.2 cm }\) \( \Rightarrow \) \( \hspace{0.2 cm }\) ( (p \( \Rightarrow \) r) \( \Leftarrow \) (q \( \Rightarrow \) r) )
\( \hspace{0.5 cm } \Rightarrow \) Monotonic Consequent. (p \( \Rightarrow \) q) \( \hspace{0.2 cm }\) \( \Rightarrow \) \( \hspace{0.2 cm }\) ( (r \( \Rightarrow \) p) \( \Rightarrow \) (r \( \Rightarrow \) q) )
\( \hspace{0.5 cm } \forall \) Antimonotonic Range. (a \( \Rightarrow \) b) \( \hspace{0.2 cm }\) \( \Rightarrow \) \( \hspace{0.2 cm }\) ( ( \( \forall \)x | a : P) \( \Leftarrow \) ( \( \forall \)x | b : P))
\( \hspace{0.5 cm } \forall \) Monotonic Body. (a \( \Rightarrow \) b) \( \hspace{0.2 cm }\) \( \Rightarrow \) \( \hspace{0.2 cm }\) ( ( \( \forall \)x | R : a) \( \Rightarrow \) ( \( \forall \)x | R : b))
\( \hspace{0.5 cm } \exists \) Monotonic Range. (a \( \Rightarrow \) b) \( \hspace{0.2 cm }\) \( \Rightarrow \) \( \hspace{0.2 cm }\) ( ( \( \exists \)x | a : P) \( \Rightarrow \) ( \( \exists \)x | b : P))
\( \hspace{0.5 cm } \exists \) Monotonic Body. (a \( \Rightarrow \) b) \( \hspace{0.2 cm }\) \( \Rightarrow \) \( \hspace{0.2 cm }\) ( ( \( \exists \)x | R : a) \( \Rightarrow \) ( \( \exists \)x | R : b))
(c) Capture Avoiding Substitution
( E[z := P ] denotes capture-avoiding substitution: E[z := P ] is a copy of expression E in which all occurrences of *free* variable z have been replaced by expression P , with names of dummies (bound variables) being first replaced to avoid capture.) (Note: best way to avoid this in practice is to have no names in common, bound or not, between P and E. If programming this substitution, then better to rename only bound vars)
(d) Monotonic and Antimonotonic Positions
Consider an occurrence of free variable z in a formula E (but not within an operand of \( \equiv \) ). The *position* of z within E is called monotonic if it is nested within an even number of negations, antecedents, or ranges of universal quantifications; otherwise, it is antimonotonic.
(e) Detailed Method for determining the monotonicity of a position
(1) Replace ( \( \forall \)x | \( F_1 \) : \( F_2 \) ) \( \hspace{0.2 cm }\) by \( \hspace{0.2 cm }\) \( \neg \)( \( \exists \)x | \( F_1 \) : \(\neg F_2 \) )
(2) Replace ( \( \exists \)x | \( F_1 \) : \( F_2 \) ) \( \hspace{0.2 cm }\) by \( \hspace{0.2 cm }\) ( \( \exists \)x |: \( F_1 \wedge F_2 \) )
(3) Replace ( \( F_1 \nLeftarrow F_2 \) ) \( \hspace{0.2 cm }\) by \( \hspace{0.2 cm }\) \( \neg \)( \( F_1 \Leftarrow F_2 \) )
(4) Replace ( \( F_1 \nRightarrow F_2 \) ) \( \hspace{0.2 cm }\) by \( \hspace{0.2 cm }\) \( \neg \)( \( F_1 \Rightarrow F_2 \) )
(5) Replace ( \( F_1 \Leftarrow F_2 \) ) \( \hspace{0.2 cm }\) by \( \hspace{0.2 cm }\) ( \( F_2 \Rightarrow F_1 \) )
(6) Replace ( \( F_1 \Rightarrow F_2 \) ) \( \hspace{0.2 cm }\) by\( \hspace{0.2 cm }\) ( \( \neg F_1 \vee F_2 \) )
(7) Replace ( \( F_1 \wedge F_2 \) ) \( \hspace{0.2 cm }\) by\( \hspace{0.2 cm }\) ( \( \neg (\neg F_1 \vee \neg F_2) \) )
(8) If z is in the second operand \( F_2 \) of ( \( F_1 \vee F_2 \) ), replace ( \( F_1 \vee F_2 \) ) by ( \( F_2 \vee F_1 \) )
(9) Count the number of \( \neg \)s in enclosing z. (the enclosing \( \forall \)s and \( \Rightarrow \)s have been transformed away by steps 1 through 8). If the number is even then positonOf(z) is monotonic and if odd then positionOf(z) is antimonotonic.
(e) MetaTheorem Monotonicity
Suppose P \( \Rightarrow \) Q is a theorem. Let E contain exactly one occurrence of free variable z (but not within an operand of \( \equiv \) ). Then
(a)If postionOf(z) is monotonic, then E[ z := P ] \( \Rightarrow \) E[ z := Q ]
(b)If postionOf(z) is monotonic, then E[ z := P ] \( \Leftarrow \) E[ z := Q ]
This also works if there are multiple occurrences of z, but they all have either monotonic xor antimonotonic positions
(f) Expressing Metatheorem Monotonicity as inference rules
(1) \( \frac{P \Rightarrow Q \hspace{0.2 cm} \wedge \hspace{0.2 cm } position \hspace{0.2 cm } of \hspace{0.2 cm } z \hspace{0.2 cm } is \hspace{0.2 cm } monotonic}{E[ z := P ] \hspace{0.2 cm } \Rightarrow \hspace{0.2 cm } E[ z := Q ]} \)
(2) \( \frac{P \Rightarrow Q \hspace{0.2 cm} \wedge \hspace{0.2 cm } position \hspace{0.2 cm } of \hspace{0.2 cm } z \hspace{0.2 cm } is \hspace{0.2 cm } antimonotonic}{E[ z := P ] \hspace{0.2 cm } \Leftarrow \hspace{0.2 cm } E[ z := Q ]} \)
(g) Convention for citing monotonicity in proofs
\( \hspace{2 cm } (\forall x |: P \wedge R) \)
\( \Rightarrow \hspace{0.5 cm } \) Monotonicity, weakening P \( \Rightarrow \) P \( \vee \) Q
\( \hspace{2 cm } (\forall x |: (P \vee Q) \wedge R) \)
Explanation: Consider \( ( \forall x |: P \wedge R) \) to be E \( \equiv \) \( (\forall x |: z \wedge R) \) and use P \( \Rightarrow \) P \( \vee \) Q as the implication in the Monotonicity Metatheorem. (the position of z is monotonic since it is the body position of a \( \forall \) )
(h) Examples
(1) Given One Point Rule, ie, ( \( \forall \) x | x = E : P) \( \equiv \) P [x := E ] and x does not occur free in E , prove Instantiation theorem, ie, Prove \( (\forall x |: P) \Rightarrow P [ x := E ] \)
Old proof, without monotonicity
LHS \( \hspace{2 cm } (\forall x |: P) \)
= \( \hspace{0.5 cm } \) notation expansion
\( \hspace{2 cm } (\forall x | true : P) \)
= \( \hspace{0.5 cm } \) true \( \equiv a \vee \neg a \)
\( \hspace{2 cm } (\forall x | (x = E) \vee (x \neq E) : P) \)
= \( \hspace{0.5 cm } \) Axiom: Range Split \( (\star | R \vee S: P) \equiv (\star | R : P) \star (\star | S : P) \) here \( \star = \wedge. \) notated as \( \forall \)
\( \hspace{2 cm } (\forall x | (x = E) : P) \wedge (\forall x | (x \neq E) : P) \)
\( \Rightarrow \hspace{0.5 cm } Theorem: a \wedge b \Rightarrow a \)
\( \hspace{2 cm } (\forall x | (x = E) : P) \)
= \( \hspace{0.5 cm } \) Single Point Axiom \( (\star y | (y = F) : Q) \equiv \) Q [ y := F ]
\( \hspace{2 cm } \) P [ x := E ] = RHS.
QED
new proof (using monotonicity)
LHS \( \hspace{2 cm } (\forall x |: P) \)
= \( \hspace{0.5 cm } \) notation expansion
\( \hspace{2 cm } (\forall x | true : P) \)
= \( \hspace{0.5 cm } \) Dummy Renaming ( \( \star \) x | R : P) \( \equiv \) ( \( \star \) y | R[x := y] : P [x := y]) , given y does not occur free in R or P, choose a variable m such that not occurs-free(m, [R, P])
\( \hspace{2 cm } \) ( \( \forall \) m | true : P[x := m])
\( \Rightarrow \hspace{0.5 cm } \) Monotonicity, Right Zero of \( \Rightarrow \) a \( \Rightarrow \) true \( \equiv \) true for any a . Let a = ( m = E) . position of true is anti monotonic
\( \hspace{2 cm }\) ( \(\forall\) m | (m = E) : P[x := m])
= \( \hspace{0.5 cm } \) Single Point theorem, given.
\( \hspace{2 cm }\) P[x := m][m := E]
= \( \hspace{0.5 cm } \) Successive textual replacement
\( \hspace{2 cm } \) P[x := E] QED
Note: implications with true or false in them are useful.
Example 2: All men are mortal, Socrates is a man. Therefore Socrates is mortal.
step 1: establish notation.
man.m : person m is a man
mortal.m : person m is a mortal
S : Socrates
step 2: formalize English to logic
( \( \forall \) m |: man.m \( \Rightarrow \) mortal.m) \( \wedge \) man.S \( \Rightarrow \) mortal.S
step 3: prove
LHS \( \hspace{2 cm } \) ( \( \forall \) m |: man.m \( \Rightarrow \) mortal.m) \( \wedge \) man.S \( \Rightarrow \) mortal.S
\( \Rightarrow \hspace{0.5 cm } \) Monotonicity, Instantiation \( (\forall x |: P) \Rightarrow P [ x := e ] \), e = S, \( \wedge \) is monotonic in both arguments
\( \hspace{2 cm } \) (man.S \( \Rightarrow \) mortal.S) \( \wedge \) man.S
\( \Rightarrow \hspace{0.5 cm } \) Modus Ponens
\( \hspace{2 cm } \) mortal.S QED
Example 3
Prove
None but those with hearts can love. Some liars are heartless. Some liars cannot love
Step 1:Establish notation
hh.p = p has a heart
cl.p = p can love
li.p = p is a liar
Step 2: Translate English to logic
( \( \forall \) p|: \( \neg \)hh.p \( \Rightarrow \) \( \neg \) cl.p ) \( \wedge \) ( \( \exists \)x |: li.x \( \wedge \) \( \neg \) hh.x ) \( \Rightarrow \) ( \( \exists \) y |: li.y \( \wedge \neg\) cl.y)
Step 3 Prove
LHS \( \hspace{2 cm } \) ( \( \forall \) p|: \( \neg \)hh.p \( \Rightarrow \) \( \neg \) cl.p ) \( \wedge \) ( \( \exists \)x |: li.x \( \wedge \) \( \neg \) hh.x )
= \( \hspace{0.5 cm } \) Theorem: Contrapositive p \( \Rightarrow \) q \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) \( \neg \)q \( \Rightarrow \) \( \neg \) p
\( \hspace{2 cm } \) ( \( \forall \) p|: cl.p \( \Rightarrow \) hh.p ) \( \wedge \) ( \( \exists \)x |: li.x \( \wedge \) \( \neg \) hh.x )
= \( \hspace{0.5 cm } \) Theorem Distribution of \( \wedge \) over \( \exists \), P \( \wedge \) ( \( \exists \) x | R : Q ) \( \equiv \) ( \( \exists \) x | R : P \( \wedge \) Q )
\( \hspace{2 cm } \) ( \( \exists \)x |: ( \( \forall \) p|: cl.p \( \Rightarrow \) hh.p ) \( \wedge \) li.x \( \wedge \) \( \neg \) hh.x )
= \( \hspace{0.5 cm } \) Monotonicity, Instantiation with (p = x), \( \wedge \) is monotonic in both arguments
\( \hspace{2 cm } \) ( \( \exists \) x|: (cl.x \( \Rightarrow \) hh.x) \( \wedge \) li.x \( \wedge \) \( \neg \) hh.x )
= \( \hspace{0.5 cm } \) Theorem: Contrapositive p \( \Rightarrow \) q \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) \( \neg \)q \( \Rightarrow \) \( \neg \) p
\( \hspace{2 cm } \) ( \( \exists \) x |: (\( \neg \) hh.x \( \Rightarrow \) \( \neg \) cl.x) \( \wedge \) li.x \( \wedge \) \( \neg \) hh.x )
\( \hspace{0.5 cm } \) \( \Rightarrow \hspace{0.5 cm } \) Modus Ponens
\( \hspace{2 cm } \) ( \( \exists \) x |: \( \neg \) cl.x \( \wedge \) li.x)
= \( \hspace{0.5 cm } \) Translate to English
\( \hspace{2 cm } \) There exists some people who are liars and also can't love = Some liars can't love QED
A function f is monotonic in its argument \( \equiv \) (x \( \Rightarrow \) y) \( \hspace{0.2 cm } \Rightarrow \hspace{0.2 cm } \) (f.x \( \Rightarrow \) f.y)
Note: The textual substitution approach in the Inference Rules provided below are a better way to work out monotonicity etc than a 'function' approach using above idea.
A function is anti-monotonic in its argument \( \equiv \) (x \( \Rightarrow \) y) \( \hspace{0.2 cm } \Rightarrow \hspace{0.2 cm } \) (f.x \( \Leftarrow \) f.y)
(b) Monotonicity of Logical Operators
\( \hspace{0.5 cm } \vee \) Monotonic. (p \( \Rightarrow \) q) \( \hspace{0.2 cm } \Rightarrow \hspace{0.2 cm } \) (p \( \vee \) r) \( \Rightarrow \) (q \( \vee \) r )
\( \hspace{0.5 cm } \wedge \) Monotonic. (p \( \Rightarrow \) q) \( \hspace{0.2 cm } \Rightarrow \hspace{0.2 cm } \) (p \( \wedge \) r) \( \Rightarrow \) (q \( \wedge \) r )
\( \hspace{0.5 cm } \neg \) Antimonotonic. (p \( \Rightarrow \) q) \( \hspace{0.2 cm } \Rightarrow \hspace{0.2 cm } \) ( \( \neg \) p \( \Leftarrow \) \( \neg \) q )
\( \hspace{0.5 cm } \Rightarrow \) Antimonotonic Antecedent. (p \( \Rightarrow \) q) \( \hspace{0.2 cm }\) \( \Rightarrow \) \( \hspace{0.2 cm }\) ( (p \( \Rightarrow \) r) \( \Leftarrow \) (q \( \Rightarrow \) r) )
\( \hspace{0.5 cm } \Rightarrow \) Monotonic Consequent. (p \( \Rightarrow \) q) \( \hspace{0.2 cm }\) \( \Rightarrow \) \( \hspace{0.2 cm }\) ( (r \( \Rightarrow \) p) \( \Rightarrow \) (r \( \Rightarrow \) q) )
\( \hspace{0.5 cm } \forall \) Antimonotonic Range. (a \( \Rightarrow \) b) \( \hspace{0.2 cm }\) \( \Rightarrow \) \( \hspace{0.2 cm }\) ( ( \( \forall \)x | a : P) \( \Leftarrow \) ( \( \forall \)x | b : P))
\( \hspace{0.5 cm } \forall \) Monotonic Body. (a \( \Rightarrow \) b) \( \hspace{0.2 cm }\) \( \Rightarrow \) \( \hspace{0.2 cm }\) ( ( \( \forall \)x | R : a) \( \Rightarrow \) ( \( \forall \)x | R : b))
\( \hspace{0.5 cm } \exists \) Monotonic Range. (a \( \Rightarrow \) b) \( \hspace{0.2 cm }\) \( \Rightarrow \) \( \hspace{0.2 cm }\) ( ( \( \exists \)x | a : P) \( \Rightarrow \) ( \( \exists \)x | b : P))
\( \hspace{0.5 cm } \exists \) Monotonic Body. (a \( \Rightarrow \) b) \( \hspace{0.2 cm }\) \( \Rightarrow \) \( \hspace{0.2 cm }\) ( ( \( \exists \)x | R : a) \( \Rightarrow \) ( \( \exists \)x | R : b))
(c) Capture Avoiding Substitution
( E[z := P ] denotes capture-avoiding substitution: E[z := P ] is a copy of expression E in which all occurrences of *free* variable z have been replaced by expression P , with names of dummies (bound variables) being first replaced to avoid capture.) (Note: best way to avoid this in practice is to have no names in common, bound or not, between P and E. If programming this substitution, then better to rename only bound vars)
(d) Monotonic and Antimonotonic Positions
Consider an occurrence of free variable z in a formula E (but not within an operand of \( \equiv \) ). The *position* of z within E is called monotonic if it is nested within an even number of negations, antecedents, or ranges of universal quantifications; otherwise, it is antimonotonic.
(e) Detailed Method for determining the monotonicity of a position
(1) Replace ( \( \forall \)x | \( F_1 \) : \( F_2 \) ) \( \hspace{0.2 cm }\) by \( \hspace{0.2 cm }\) \( \neg \)( \( \exists \)x | \( F_1 \) : \(\neg F_2 \) )
(2) Replace ( \( \exists \)x | \( F_1 \) : \( F_2 \) ) \( \hspace{0.2 cm }\) by \( \hspace{0.2 cm }\) ( \( \exists \)x |: \( F_1 \wedge F_2 \) )
(3) Replace ( \( F_1 \nLeftarrow F_2 \) ) \( \hspace{0.2 cm }\) by \( \hspace{0.2 cm }\) \( \neg \)( \( F_1 \Leftarrow F_2 \) )
(4) Replace ( \( F_1 \nRightarrow F_2 \) ) \( \hspace{0.2 cm }\) by \( \hspace{0.2 cm }\) \( \neg \)( \( F_1 \Rightarrow F_2 \) )
(5) Replace ( \( F_1 \Leftarrow F_2 \) ) \( \hspace{0.2 cm }\) by \( \hspace{0.2 cm }\) ( \( F_2 \Rightarrow F_1 \) )
(6) Replace ( \( F_1 \Rightarrow F_2 \) ) \( \hspace{0.2 cm }\) by\( \hspace{0.2 cm }\) ( \( \neg F_1 \vee F_2 \) )
(7) Replace ( \( F_1 \wedge F_2 \) ) \( \hspace{0.2 cm }\) by\( \hspace{0.2 cm }\) ( \( \neg (\neg F_1 \vee \neg F_2) \) )
(8) If z is in the second operand \( F_2 \) of ( \( F_1 \vee F_2 \) ), replace ( \( F_1 \vee F_2 \) ) by ( \( F_2 \vee F_1 \) )
(9) Count the number of \( \neg \)s in enclosing z. (the enclosing \( \forall \)s and \( \Rightarrow \)s have been transformed away by steps 1 through 8). If the number is even then positonOf(z) is monotonic and if odd then positionOf(z) is antimonotonic.
(e) MetaTheorem Monotonicity
Suppose P \( \Rightarrow \) Q is a theorem. Let E contain exactly one occurrence of free variable z (but not within an operand of \( \equiv \) ). Then
(a)If postionOf(z) is monotonic, then E[ z := P ] \( \Rightarrow \) E[ z := Q ]
(b)If postionOf(z) is monotonic, then E[ z := P ] \( \Leftarrow \) E[ z := Q ]
This also works if there are multiple occurrences of z, but they all have either monotonic xor antimonotonic positions
(f) Expressing Metatheorem Monotonicity as inference rules
(1) \( \frac{P \Rightarrow Q \hspace{0.2 cm} \wedge \hspace{0.2 cm } position \hspace{0.2 cm } of \hspace{0.2 cm } z \hspace{0.2 cm } is \hspace{0.2 cm } monotonic}{E[ z := P ] \hspace{0.2 cm } \Rightarrow \hspace{0.2 cm } E[ z := Q ]} \)
(2) \( \frac{P \Rightarrow Q \hspace{0.2 cm} \wedge \hspace{0.2 cm } position \hspace{0.2 cm } of \hspace{0.2 cm } z \hspace{0.2 cm } is \hspace{0.2 cm } antimonotonic}{E[ z := P ] \hspace{0.2 cm } \Leftarrow \hspace{0.2 cm } E[ z := Q ]} \)
(g) Convention for citing monotonicity in proofs
\( \hspace{2 cm } (\forall x |: P \wedge R) \)
\( \Rightarrow \hspace{0.5 cm } \) Monotonicity, weakening P \( \Rightarrow \) P \( \vee \) Q
\( \hspace{2 cm } (\forall x |: (P \vee Q) \wedge R) \)
Explanation: Consider \( ( \forall x |: P \wedge R) \) to be E \( \equiv \) \( (\forall x |: z \wedge R) \) and use P \( \Rightarrow \) P \( \vee \) Q as the implication in the Monotonicity Metatheorem. (the position of z is monotonic since it is the body position of a \( \forall \) )
(h) Examples
(1) Given One Point Rule, ie, ( \( \forall \) x | x = E : P) \( \equiv \) P [x := E ] and x does not occur free in E , prove Instantiation theorem, ie, Prove \( (\forall x |: P) \Rightarrow P [ x := E ] \)
Old proof, without monotonicity
LHS \( \hspace{2 cm } (\forall x |: P) \)
= \( \hspace{0.5 cm } \) notation expansion
\( \hspace{2 cm } (\forall x | true : P) \)
= \( \hspace{0.5 cm } \) true \( \equiv a \vee \neg a \)
\( \hspace{2 cm } (\forall x | (x = E) \vee (x \neq E) : P) \)
= \( \hspace{0.5 cm } \) Axiom: Range Split \( (\star | R \vee S: P) \equiv (\star | R : P) \star (\star | S : P) \) here \( \star = \wedge. \) notated as \( \forall \)
\( \hspace{2 cm } (\forall x | (x = E) : P) \wedge (\forall x | (x \neq E) : P) \)
\( \Rightarrow \hspace{0.5 cm } Theorem: a \wedge b \Rightarrow a \)
\( \hspace{2 cm } (\forall x | (x = E) : P) \)
= \( \hspace{0.5 cm } \) Single Point Axiom \( (\star y | (y = F) : Q) \equiv \) Q [ y := F ]
\( \hspace{2 cm } \) P [ x := E ] = RHS.
QED
new proof (using monotonicity)
LHS \( \hspace{2 cm } (\forall x |: P) \)
= \( \hspace{0.5 cm } \) notation expansion
\( \hspace{2 cm } (\forall x | true : P) \)
= \( \hspace{0.5 cm } \) Dummy Renaming ( \( \star \) x | R : P) \( \equiv \) ( \( \star \) y | R[x := y] : P [x := y]) , given y does not occur free in R or P, choose a variable m such that not occurs-free(m, [R, P])
\( \hspace{2 cm } \) ( \( \forall \) m | true : P[x := m])
\( \Rightarrow \hspace{0.5 cm } \) Monotonicity, Right Zero of \( \Rightarrow \) a \( \Rightarrow \) true \( \equiv \) true for any a . Let a = ( m = E) . position of true is anti monotonic
\( \hspace{2 cm }\) ( \(\forall\) m | (m = E) : P[x := m])
= \( \hspace{0.5 cm } \) Single Point theorem, given.
\( \hspace{2 cm }\) P[x := m][m := E]
= \( \hspace{0.5 cm } \) Successive textual replacement
\( \hspace{2 cm } \) P[x := E] QED
Note: implications with true or false in them are useful.
Example 2: All men are mortal, Socrates is a man. Therefore Socrates is mortal.
step 1: establish notation.
man.m : person m is a man
mortal.m : person m is a mortal
S : Socrates
step 2: formalize English to logic
( \( \forall \) m |: man.m \( \Rightarrow \) mortal.m) \( \wedge \) man.S \( \Rightarrow \) mortal.S
step 3: prove
LHS \( \hspace{2 cm } \) ( \( \forall \) m |: man.m \( \Rightarrow \) mortal.m) \( \wedge \) man.S \( \Rightarrow \) mortal.S
\( \Rightarrow \hspace{0.5 cm } \) Monotonicity, Instantiation \( (\forall x |: P) \Rightarrow P [ x := e ] \), e = S, \( \wedge \) is monotonic in both arguments
\( \hspace{2 cm } \) (man.S \( \Rightarrow \) mortal.S) \( \wedge \) man.S
\( \Rightarrow \hspace{0.5 cm } \) Modus Ponens
\( \hspace{2 cm } \) mortal.S QED
Example 3
Prove
None but those with hearts can love. Some liars are heartless. Some liars cannot love
Step 1:Establish notation
hh.p = p has a heart
cl.p = p can love
li.p = p is a liar
Step 2: Translate English to logic
( \( \forall \) p|: \( \neg \)hh.p \( \Rightarrow \) \( \neg \) cl.p ) \( \wedge \) ( \( \exists \)x |: li.x \( \wedge \) \( \neg \) hh.x ) \( \Rightarrow \) ( \( \exists \) y |: li.y \( \wedge \neg\) cl.y)
Step 3 Prove
LHS \( \hspace{2 cm } \) ( \( \forall \) p|: \( \neg \)hh.p \( \Rightarrow \) \( \neg \) cl.p ) \( \wedge \) ( \( \exists \)x |: li.x \( \wedge \) \( \neg \) hh.x )
= \( \hspace{0.5 cm } \) Theorem: Contrapositive p \( \Rightarrow \) q \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) \( \neg \)q \( \Rightarrow \) \( \neg \) p
\( \hspace{2 cm } \) ( \( \forall \) p|: cl.p \( \Rightarrow \) hh.p ) \( \wedge \) ( \( \exists \)x |: li.x \( \wedge \) \( \neg \) hh.x )
= \( \hspace{0.5 cm } \) Theorem Distribution of \( \wedge \) over \( \exists \), P \( \wedge \) ( \( \exists \) x | R : Q ) \( \equiv \) ( \( \exists \) x | R : P \( \wedge \) Q )
\( \hspace{2 cm } \) ( \( \exists \)x |: ( \( \forall \) p|: cl.p \( \Rightarrow \) hh.p ) \( \wedge \) li.x \( \wedge \) \( \neg \) hh.x )
= \( \hspace{0.5 cm } \) Monotonicity, Instantiation with (p = x), \( \wedge \) is monotonic in both arguments
\( \hspace{2 cm } \) ( \( \exists \) x|: (cl.x \( \Rightarrow \) hh.x) \( \wedge \) li.x \( \wedge \) \( \neg \) hh.x )
= \( \hspace{0.5 cm } \) Theorem: Contrapositive p \( \Rightarrow \) q \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) \( \neg \)q \( \Rightarrow \) \( \neg \) p
\( \hspace{2 cm } \) ( \( \exists \) x |: (\( \neg \) hh.x \( \Rightarrow \) \( \neg \) cl.x) \( \wedge \) li.x \( \wedge \) \( \neg \) hh.x )
\( \hspace{0.5 cm } \) \( \Rightarrow \hspace{0.5 cm } \) Modus Ponens
\( \hspace{2 cm } \) ( \( \exists \) x |: \( \neg \) cl.x \( \wedge \) li.x)
= \( \hspace{0.5 cm } \) Translate to English
\( \hspace{2 cm } \) There exists some people who are liars and also can't love = Some liars can't love QED
EQ 5 Implication Axioms and Theorems
(1) Axiom: Definition of Implication: p \( \Rightarrow \) q \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p \( \vee \) q \( \equiv \) q
(2) Axiom: Consequence p \( \Leftarrow \) q \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) q \( \Rightarrow \) p
(3) Theorem: Definition of Implication p \( \Rightarrow \) q \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm }\) \( \neg \)p \( \vee \) q
(4) Theorem: Definition of Implication: p \( \Rightarrow \) q \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p \( \wedge \) q \( \equiv \) p
(5) Theorem: Contrapositive p \( \Rightarrow \) q \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) \( \neg \)q \( \Rightarrow \) \( \neg \) p
(6) Theorem: p \( \Rightarrow \) (q \( \equiv \) r)\( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p \( \wedge\) q \( \equiv \) p \( \wedge \) r
(7) Theorem: Distributivity \( \frac{\Rightarrow}{\equiv} \) p \( \Rightarrow \) (q \( \equiv \) r) \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p \( \Rightarrow \) q \( \equiv \) p \( \Rightarrow \) r
(8) Theorem: Distributivity \( \frac{\Rightarrow}{\Rightarrow} \) p \( \Rightarrow \) (q \( \Rightarrow \) r) \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) (p \( \Rightarrow \) q) \( \Rightarrow \) (p \( \Rightarrow \) r)
(9) Theorem: Shunting p \( \wedge \) q \( \Rightarrow \) r \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p \( \Rightarrow \) (q \( \Rightarrow \) r )
(10) Theorem: p \( \wedge \) ( p \( \Rightarrow \) q ) \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p \( \wedge \) q
(11) Theorem: p \( \wedge \) ( q \( \Rightarrow \) p) \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p
(12) Theorem: p \( \vee \) ( p \( \Rightarrow \) q ) \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) true
(13) Theorem: p \( \vee \) ( q \( \Rightarrow \) p) \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) q \( \Rightarrow \) p
(14) Theorem: p \( \vee \) q \( \hspace{0.2 cm } \)\( \Rightarrow \)\( \hspace{0.2 cm } \) p \( \wedge \) q \( \equiv \) p \( \equiv \) q
(15) Reflexivity of \( \Rightarrow \) : p \( \Rightarrow \) p \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) true
(16) Theorem: Right Zero of \( \Rightarrow \) : p \( \Rightarrow \) true \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) true
(17) Theorem: Left Identity of \( \Rightarrow \) : true \( \Rightarrow \) p \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p
(18) Theorem: p \( \Rightarrow \) false \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) \( \neg \)p
(19) Theorem: false \( \Rightarrow \) p \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) true
Weakening and Strengthening Theorems
(20) Theorem: p \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) p \( \vee \) q
(21) Theorem: p \( \wedge \) q \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) p
(22) Theorem: p \( \wedge \) q \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) p \( \vee \) q
(23) Theorem: p \( \wedge \) q \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) p \( \wedge \) (q \( \vee \) r)
(24) Theorem: p \( \vee \) (q \( \wedge \) r) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) p \( \vee \) q
(25) Theorem: Modus Ponens p \( \wedge \) ( p \( \Rightarrow \) q) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) q
(26) Theorem : (p \( \Rightarrow \) r) \( \wedge \) (q \( \Rightarrow \) r) \( \hspace{0.2 cm } \) \( \equiv \) \( \hspace{0.2 cm } \) ( p \( \vee \) q \( \Rightarrow \) r)
(27) Theorem : (p \( \Rightarrow \) r) \( \wedge \) ( \( \neg \)p \( \Rightarrow \) r) \( \hspace{0.2 cm } \) \( \equiv \) \( \hspace{0.2 cm } \) r
(28) Theorem: Mutual Implication (p \( \Rightarrow \) q) \( \wedge \) (q \( \Rightarrow \) p) \( \hspace{0.2 cm } \) \( \equiv \) \( \hspace{0.2 cm } \) ( p \( \equiv \) q)
(29) Theorem: Anti-Symmetry (p \( \Rightarrow \) q) \( \wedge \) (q \( \Rightarrow \) p) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) ( p \( \equiv \) q)
(30) Theorem: Transitivity (1) (p \( \Rightarrow \) q) \( \wedge \) (q \( \Rightarrow \) r) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) (p \( \Rightarrow \) r)
(31) Theorem: Transitivity (2) (p \( \equiv \) q) \( \wedge \) (q \( \Rightarrow \) r) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) (p \( \Rightarrow \) r)
(32) Theorem: Transitivity (3) (p \( \Rightarrow \) q) \( \wedge \) (q \( \equiv \) r) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) (p \( \Rightarrow \) r)
Other useful Implication Theorems
(33) Theorem: p \( \Rightarrow \) ( q \( \Rightarrow \) p) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) true
(34) Theorem (p \( \Rightarrow \) q) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) (p \( \wedge \) r) \( \Rightarrow \) (q \( \wedge \) r)
(35) Theorem (p \( \Rightarrow \) q) \( \wedge \) (r \( \Rightarrow \) s) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) (p \( \vee \) r) \( \Rightarrow \) (q \( \vee \) s)
(36) Theorem (p \( \Rightarrow \) q) \( \wedge \) (r \( \Rightarrow \) s) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) (p \( \wedge \) r) \( \Rightarrow \) (q \( \wedge \) s)
(37) Theorem a \( \Rightarrow \) \( \neg \)b \( \hspace{0.2 cm } \) \( \equiv \) \( \hspace{0.2 cm } \) a \( \Rightarrow \) b \( \equiv \) \( \neg \)a
(38) Theorem \( \neg \)a \( \Rightarrow \) b \( \hspace{0.2 cm } \) \( \equiv \) \( \hspace{0.2 cm } \) a \( \Rightarrow \) b \( \equiv \) b
(2) Axiom: Consequence p \( \Leftarrow \) q \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) q \( \Rightarrow \) p
(3) Theorem: Definition of Implication p \( \Rightarrow \) q \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm }\) \( \neg \)p \( \vee \) q
(4) Theorem: Definition of Implication: p \( \Rightarrow \) q \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p \( \wedge \) q \( \equiv \) p
(5) Theorem: Contrapositive p \( \Rightarrow \) q \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) \( \neg \)q \( \Rightarrow \) \( \neg \) p
(6) Theorem: p \( \Rightarrow \) (q \( \equiv \) r)\( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p \( \wedge\) q \( \equiv \) p \( \wedge \) r
(7) Theorem: Distributivity \( \frac{\Rightarrow}{\equiv} \) p \( \Rightarrow \) (q \( \equiv \) r) \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p \( \Rightarrow \) q \( \equiv \) p \( \Rightarrow \) r
(8) Theorem: Distributivity \( \frac{\Rightarrow}{\Rightarrow} \) p \( \Rightarrow \) (q \( \Rightarrow \) r) \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) (p \( \Rightarrow \) q) \( \Rightarrow \) (p \( \Rightarrow \) r)
(9) Theorem: Shunting p \( \wedge \) q \( \Rightarrow \) r \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p \( \Rightarrow \) (q \( \Rightarrow \) r )
(10) Theorem: p \( \wedge \) ( p \( \Rightarrow \) q ) \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p \( \wedge \) q
(11) Theorem: p \( \wedge \) ( q \( \Rightarrow \) p) \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p
(12) Theorem: p \( \vee \) ( p \( \Rightarrow \) q ) \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) true
(13) Theorem: p \( \vee \) ( q \( \Rightarrow \) p) \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) q \( \Rightarrow \) p
(14) Theorem: p \( \vee \) q \( \hspace{0.2 cm } \)\( \Rightarrow \)\( \hspace{0.2 cm } \) p \( \wedge \) q \( \equiv \) p \( \equiv \) q
(15) Reflexivity of \( \Rightarrow \) : p \( \Rightarrow \) p \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) true
(16) Theorem: Right Zero of \( \Rightarrow \) : p \( \Rightarrow \) true \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) true
(17) Theorem: Left Identity of \( \Rightarrow \) : true \( \Rightarrow \) p \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) p
(18) Theorem: p \( \Rightarrow \) false \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) \( \neg \)p
(19) Theorem: false \( \Rightarrow \) p \( \hspace{0.2 cm } \)\( \equiv \)\( \hspace{0.2 cm } \) true
Weakening and Strengthening Theorems
(20) Theorem: p \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) p \( \vee \) q
(21) Theorem: p \( \wedge \) q \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) p
(22) Theorem: p \( \wedge \) q \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) p \( \vee \) q
(23) Theorem: p \( \wedge \) q \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) p \( \wedge \) (q \( \vee \) r)
(24) Theorem: p \( \vee \) (q \( \wedge \) r) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) p \( \vee \) q
(25) Theorem: Modus Ponens p \( \wedge \) ( p \( \Rightarrow \) q) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) q
(26) Theorem : (p \( \Rightarrow \) r) \( \wedge \) (q \( \Rightarrow \) r) \( \hspace{0.2 cm } \) \( \equiv \) \( \hspace{0.2 cm } \) ( p \( \vee \) q \( \Rightarrow \) r)
(27) Theorem : (p \( \Rightarrow \) r) \( \wedge \) ( \( \neg \)p \( \Rightarrow \) r) \( \hspace{0.2 cm } \) \( \equiv \) \( \hspace{0.2 cm } \) r
(28) Theorem: Mutual Implication (p \( \Rightarrow \) q) \( \wedge \) (q \( \Rightarrow \) p) \( \hspace{0.2 cm } \) \( \equiv \) \( \hspace{0.2 cm } \) ( p \( \equiv \) q)
(29) Theorem: Anti-Symmetry (p \( \Rightarrow \) q) \( \wedge \) (q \( \Rightarrow \) p) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) ( p \( \equiv \) q)
(30) Theorem: Transitivity (1) (p \( \Rightarrow \) q) \( \wedge \) (q \( \Rightarrow \) r) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) (p \( \Rightarrow \) r)
(31) Theorem: Transitivity (2) (p \( \equiv \) q) \( \wedge \) (q \( \Rightarrow \) r) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) (p \( \Rightarrow \) r)
(32) Theorem: Transitivity (3) (p \( \Rightarrow \) q) \( \wedge \) (q \( \equiv \) r) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) (p \( \Rightarrow \) r)
Other useful Implication Theorems
(33) Theorem: p \( \Rightarrow \) ( q \( \Rightarrow \) p) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) true
(34) Theorem (p \( \Rightarrow \) q) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) (p \( \wedge \) r) \( \Rightarrow \) (q \( \wedge \) r)
(35) Theorem (p \( \Rightarrow \) q) \( \wedge \) (r \( \Rightarrow \) s) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) (p \( \vee \) r) \( \Rightarrow \) (q \( \vee \) s)
(36) Theorem (p \( \Rightarrow \) q) \( \wedge \) (r \( \Rightarrow \) s) \( \hspace{0.2 cm } \) \( \Rightarrow \) \( \hspace{0.2 cm } \) (p \( \wedge \) r) \( \Rightarrow \) (q \( \wedge \) s)
(37) Theorem a \( \Rightarrow \) \( \neg \)b \( \hspace{0.2 cm } \) \( \equiv \) \( \hspace{0.2 cm } \) a \( \Rightarrow \) b \( \equiv \) \( \neg \)a
(38) Theorem \( \neg \)a \( \Rightarrow \) b \( \hspace{0.2 cm } \) \( \equiv \) \( \hspace{0.2 cm } \) a \( \Rightarrow \) b \( \equiv \) b
Saturday, October 1, 2011
EQ 4 Equality vs Equivalence
b \( \equiv\) c is evaluated the same as b = c (in terms of truth tables) except that \( \equiv \) is allowed only when b and c are booleans.
Definition of Conjunctional
If \( \circ \) and \( \star \) are conjunctional operators, b \( \circ \) c \( \star \) d is equivalent to b \( \circ \) c \( \wedge \) c \( \star \) d.
From the precedence table, all operators on line 10 are conjunctional, ie = < > \( \epsilon \) \( \subset \) \( \subseteq \) \( \supset \) \( \supseteq \) | are all conjunctional
Definition of Associative
Binary Operator \( \circ \) is associative \( \equiv \) ((b \( \circ \) c) \( \circ \) d) = (b \( \circ \) ( c \( \circ \) d ))
Key 1: \( \equiv \) is associative, = is conjunctional
Key 2: Conjunctional use of = (and other conjunctional operators ) are syntactic sugar.
Conversion back and forth:
\( \hspace{2 cm }\) b \( \equiv \) c \( \equiv \) d
= \( \hspace{0.5 cm } \) parenthesize
\( \hspace{2 cm }\) (b \( \equiv \) c ) \( \equiv \) d
= \( \hspace{0.5 cm } \) replace operator
\( \hspace{2 cm } \) (b = c) = d
and
\( \hspace{2 cm }\) b = c = d
= \( \hspace{0.5 cm } \) remove conjunctional syntactic sugar
\( \hspace{2 cm }\) b = c \( \wedge \) c = d
= \( \hspace{0.5 cm } \) parenthesize
\( \hspace{2 cm }\) (b = c) \( \wedge \) (c = d)
= \( \hspace{0.5 cm } \) replace operator
\( \hspace{2 cm }\) (b \( \equiv \) c) \( \wedge \) (c \( \equiv \) d)
Definition of Conjunctional
If \( \circ \) and \( \star \) are conjunctional operators, b \( \circ \) c \( \star \) d is equivalent to b \( \circ \) c \( \wedge \) c \( \star \) d.
From the precedence table, all operators on line 10 are conjunctional, ie = < > \( \epsilon \) \( \subset \) \( \subseteq \) \( \supset \) \( \supseteq \) | are all conjunctional
Definition of Associative
Binary Operator \( \circ \) is associative \( \equiv \) ((b \( \circ \) c) \( \circ \) d) = (b \( \circ \) ( c \( \circ \) d ))
Key 1: \( \equiv \) is associative, = is conjunctional
Key 2: Conjunctional use of = (and other conjunctional operators ) are syntactic sugar.
Conversion back and forth:
\( \hspace{2 cm }\) b \( \equiv \) c \( \equiv \) d
= \( \hspace{0.5 cm } \) parenthesize
\( \hspace{2 cm }\) (b \( \equiv \) c ) \( \equiv \) d
= \( \hspace{0.5 cm } \) replace operator
\( \hspace{2 cm } \) (b = c) = d
and
\( \hspace{2 cm }\) b = c = d
= \( \hspace{0.5 cm } \) remove conjunctional syntactic sugar
\( \hspace{2 cm }\) b = c \( \wedge \) c = d
= \( \hspace{0.5 cm } \) parenthesize
\( \hspace{2 cm }\) (b = c) \( \wedge \) (c = d)
= \( \hspace{0.5 cm } \) replace operator
\( \hspace{2 cm }\) (b \( \equiv \) c) \( \wedge \) (c \( \equiv \) d)
EQ 3: Inference Rules
The logic EQ has four inference rules
(1) Substitution
\( \frac{E}{E[v := F]} \)
where E is an expression, v is a list of variables and F is a corresponding list of expressions.
Iow, if E is a theorem, so is E with all the variables in V replaced by the corresponding expressions in F.
E.g: Let E be 2.x/2 = x be a theorem.
Then by substitution, so is 2.(j + 5) / 2 = j + 5 where v=x and E = j+5
(2) Leibniz
\( \frac{X=Y}{E[z:=X]=E[z:=Y]} \)
NB: z is a variable, NOT an expression.
Two ways of looking at Leibniz
(A) Given an equality X = Y and an expression E,
(1) Choose a variable z within E
(2) Replace the equality with a new equality with z replaced by X on one side and Y on the other
(B) Given E,
(1) spot an *expression X* (NOT variable ) within E that needs replacement
(2) Find an equality X = Y
(3) consider the given expression E to be actually E [z := X]
(4) Use Leibniz with the equality (from (2) ) to get E [z := Y]
this is written as
\( \hspace{2 cm } E[z:=X] \)
= \( \hspace{0.5 cm } \) Leibniz. z is z. X = Y
\( \hspace{2 cm } E[z:=Y \)
eg:
Given m = 2j (note: this is the equality X = Y) and E is m/2 = 2.(j - 1) prove that 2j/2 = 2(j-1)
Leibniz usage B: m on the LHS of E needs to be replaced with 2j, so we look for an equality with m on the left side, which we find in the given equality. If we consider the LHS of E to be E[z := m], then
\( \hspace{2 cm } m/2 = 2(j - 1) \)
= \( \hspace{0.5 cm } \) Leibniz. z is m, m = 2j
\( \hspace{2 cm } 2j/2 = 2(j - 1) \)
(C) Combined use of Substitution and Leibniz
Strictly speaking, Substitution and Leibniz are distinct inference rules and the two should be used distinctly
Given we know that 2x/2 = x (note: this is the equality X=Y)
let E be 2j/2 = 2(j+1). prove j = 2(j-1 )
(separate use of Substitution and Leibniz)
\( \hspace{2 cm }E \equiv \) 2j/2 = 2(j - 1)
= \( \hspace{0.5 cm } \) Substitution j := x
\( \hspace{2 cm }\) 2x/2 = 2(x - 1)
= \( \hspace{0.5 cm } \) Leibniz z is 2x/2 with equality 2x/2 = x
\( \hspace{2 cm } \) x = 2(x - 1)
= \( \hspace{0.5 cm } \) Substitution x := j
\( \hspace{2 cm } \)j = 2(j - 1) QED
(simultaneous use of Substitution and Leibniz collapses some steps)
\( \hspace{2 cm }E \equiv \) 2j/2 = 2(j - 1)
= \( \hspace{0.5 cm } \) Substitution and Leibniz 2x/2:= x
\( \hspace{2 cm } \)j = 2(j - 1) QED
(3) Transitivity
\( \frac{X=Y,Y=Z}{X=Z} \)
iow if X = Y and Y = Z are theorems, so is X = Z
(4) Equanimity
\( \frac{E,E=F}{F} \)
iow a theorem is either an axiom or the result of an inference rule where the premises are axioms
Example for use of all 4 inference rules
Prove that \( \neg p \equiv p \equiv false \)
Proof:
(0) \( \hspace{2 cm } \neg p \equiv p \equiv false \)
(1) = \( \hspace{0.5 cm } \) Leibniz and Substitution with Theorem \(\neg (x \equiv y) \equiv \neg x \equiv y \) used in the reverse direction, substituting x,y := p,p and z = \(\neg p \equiv p \)
(2) \( \hspace{2 cm } \neg (p \equiv p) \equiv\) false
(3) = \( \hspace{0.5 cm } \) Leib + Sub using Theorem Identity of \( \equiv \),\( x \equiv x \equiv \) true , z is p \( \equiv \) p, and x := p
(4) \( \hspace{2 cm } \neg true \equiv false \)
(3) = \( \hspace{0.5 cm } \) is an Axiom and therefore
(5) \( \hspace{2 cm } \) true QED
and since (0) = (2) and (2) = (4) and (4) = (5), by Transitivity (0) = (4)
and since (0) = (4) and (4) is a theorem, (0) is a theorem by Equanimity.
(1) Substitution
\( \frac{E}{E[v := F]} \)
where E is an expression, v is a list of variables and F is a corresponding list of expressions.
Iow, if E is a theorem, so is E with all the variables in V replaced by the corresponding expressions in F.
E.g: Let E be 2.x/2 = x be a theorem.
Then by substitution, so is 2.(j + 5) / 2 = j + 5 where v=x and E = j+5
(2) Leibniz
\( \frac{X=Y}{E[z:=X]=E[z:=Y]} \)
NB: z is a variable, NOT an expression.
Two ways of looking at Leibniz
(A) Given an equality X = Y and an expression E,
(1) Choose a variable z within E
(2) Replace the equality with a new equality with z replaced by X on one side and Y on the other
(B) Given E,
(1) spot an *expression X* (NOT variable ) within E that needs replacement
(2) Find an equality X = Y
(3) consider the given expression E to be actually E [z := X]
(4) Use Leibniz with the equality (from (2) ) to get E [z := Y]
this is written as
\( \hspace{2 cm } E[z:=X] \)
= \( \hspace{0.5 cm } \) Leibniz. z is z. X = Y
\( \hspace{2 cm } E[z:=Y \)
eg:
Given m = 2j (note: this is the equality X = Y) and E is m/2 = 2.(j - 1) prove that 2j/2 = 2(j-1)
Leibniz usage B: m on the LHS of E needs to be replaced with 2j, so we look for an equality with m on the left side, which we find in the given equality. If we consider the LHS of E to be E[z := m], then
\( \hspace{2 cm } m/2 = 2(j - 1) \)
= \( \hspace{0.5 cm } \) Leibniz. z is m, m = 2j
\( \hspace{2 cm } 2j/2 = 2(j - 1) \)
(C) Combined use of Substitution and Leibniz
Strictly speaking, Substitution and Leibniz are distinct inference rules and the two should be used distinctly
Given we know that 2x/2 = x (note: this is the equality X=Y)
let E be 2j/2 = 2(j+1). prove j = 2(j-1 )
(separate use of Substitution and Leibniz)
\( \hspace{2 cm }E \equiv \) 2j/2 = 2(j - 1)
= \( \hspace{0.5 cm } \) Substitution j := x
\( \hspace{2 cm }\) 2x/2 = 2(x - 1)
= \( \hspace{0.5 cm } \) Leibniz z is 2x/2 with equality 2x/2 = x
\( \hspace{2 cm } \) x = 2(x - 1)
= \( \hspace{0.5 cm } \) Substitution x := j
\( \hspace{2 cm } \)j = 2(j - 1) QED
(simultaneous use of Substitution and Leibniz collapses some steps)
\( \hspace{2 cm }E \equiv \) 2j/2 = 2(j - 1)
= \( \hspace{0.5 cm } \) Substitution and Leibniz 2x/2:= x
\( \hspace{2 cm } \)j = 2(j - 1) QED
(3) Transitivity
\( \frac{X=Y,Y=Z}{X=Z} \)
iow if X = Y and Y = Z are theorems, so is X = Z
(4) Equanimity
\( \frac{E,E=F}{F} \)
iow a theorem is either an axiom or the result of an inference rule where the premises are axioms
Example for use of all 4 inference rules
Prove that \( \neg p \equiv p \equiv false \)
Proof:
(0) \( \hspace{2 cm } \neg p \equiv p \equiv false \)
(1) = \( \hspace{0.5 cm } \) Leibniz and Substitution with Theorem \(\neg (x \equiv y) \equiv \neg x \equiv y \) used in the reverse direction, substituting x,y := p,p and z = \(\neg p \equiv p \)
(2) \( \hspace{2 cm } \neg (p \equiv p) \equiv\) false
(3) = \( \hspace{0.5 cm } \) Leib + Sub using Theorem Identity of \( \equiv \),\( x \equiv x \equiv \) true , z is p \( \equiv \) p, and x := p
(4) \( \hspace{2 cm } \neg true \equiv false \)
(3) = \( \hspace{0.5 cm } \) is an Axiom and therefore
(5) \( \hspace{2 cm } \) true QED
and since (0) = (2) and (2) = (4) and (4) = (5), by Transitivity (0) = (4)
and since (0) = (4) and (4) is a theorem, (0) is a theorem by Equanimity.
Subscribe to:
Posts (Atom)