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