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)