(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
No comments:
Post a Comment