EQ 9 Quantification

(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)