Formal Foundations of Computer Science 1 -- 4.7.2 Arithmetic Quantifiers

Go backward to 4.7.1 Minimum and Maximum
Go up to 4.7 Arithmetic Notions
Go forward to 4.7.3 Binomials

4.7.2 Arithmetic Quantifiers

Frequently we want to construct the sum of a collection of values.

Definition 56 (Sum Quantifier) If x is a variable, F is a formula and T is a term, then the following is a term with bound variable x:

(sum_{x, F} T).

The value of this term is 0, if F does not hold for any x; otherwise it is, for some x that satisfies F, the sum of the value of T and of the value of the term for all other x, i.e.,

(forall x: ~F) => (sum_{x, F} T) = 0;

(forall y: F[x <- y] => (sum_{x, F} T) = T[x <- y] + (sum_{x, F /\ x != y} T)).

Please note that the value of the term is only defined if there do not exist infinitely many x such that F holds.

Usually F contains the condition x in N, which is therefore not written explicitly. Also the variable x is usually not written but has to be deduced from the context.

Example

(sum_{1 <= i <= n} i²) = (sum_{i, (i in N /\ 1 <= i /\ i
<= n)} i²);

(sum_{1 <= i <= 5} i²) = 1²+2²+3²+4²+5²;

(sum_{1 <= i <= 0} i⁵) = 0;

(sum_{1 <= i <= 9} (x-i)²) = (x-1)² + (sum_{2 <= i <= 9} (x-i)²)

(sum_{1 <= i <= n} xⁱ) = (sum_{1 <= i <= n /\ even(i)} xⁱ) + (sum_{1 <= i <= n /\ odd(i)} xⁱ)

Example Let a := [3, 1, 2, 9, 0, 7]. We have

(sum_{0 <= i <= 5} a_i*10ⁱ) = 709213.

In general, for any finite sequence d of "decimal digits" the term

(sum_{0 <= i < length(d)} d_i*10ⁱ)

denotes the value of this sequence in the decimal number system. Likewise, for any finite sequence b of binary digits 0 and 1, the value

(sum_{0 <= i < length(b)} b_i*2ⁱ)

denotes the value of this sequence in the binary number system, e.g., the value of [0, 1, 1, 0, 1] is

1*2⁴+0*2³+1*2²+1*2¹+0*2⁰=22.

The quantifier may also bind multiple variables.

Example

(sum_{1 <= i <= 5, 1 <= j <= 3} i*j) = 1*1+1*2+1*3+ (sum_{2 <= i <= 5, 1 <= j <= 3} i*j)

(sum_{1 <= i <= 3, 1 <= j <= i} i*j) = 1*1 + 2*1 + 2*2 + 3*1 + 3*2 +3*3.

We have a number of important identities.

Proposition 58 (Sum Quantifier) For all variables i and j and formulas F (in which j does not occur freely), G (in which i does not occur freely), and H and terms T and U we have:

(sum_{i, F} T) * (sum_{j, G} U) = (sum_{i, F} (sum_{j, G} T*U)).

(sum_{i, F} (sum_{j, G} T)) = (sum_{j, G} (sum_{i, F} T)) = (sum_{i, j, F /\ G} T).

(sum_{i, F} T) + (sum_{i, H} T) = (sum_{i, F \/ H} T) + (sum_{i, F /\ H} T).

Furthermore, if term C is a term in which i does not occur freely, we have:

(sum_{i, F} C*T) = C*(sum_{i, F} T).

(sum_{i, F} C) = n*C (where n is the number of i for which F holds).

Example

(sum_{1 <= i <= n} xⁱ) * (sum_{1 <= j <= m} x^j) = (sum_{1 <= i <= n} (sum_{1 <= j <= m} x^i+j)) = (sum_{1 <= i <= n /\ 1 <= j <= m} x^i+j).

(sum_{1 <= i <= n} (sum_{1 <= j <= m} i*x^j)) = (sum_{1 <= i <= n} (i*(sum_{1 <= j <= m} x^j))).

Likewise we often wish to construct the product of a collection of values.

Definition 57 (Product Quantifier) If x is a variable, F is a formula and T is a term, then the following is a term with bound variable x:

(prod_{x, F} T).

The value of this term is 1, if F does not hold for any x; otherwise it is, for some x that satisfies F, the product of the value of T and of the value of the term for all other x, i.e.,

(forall x: ~F) => (prod_{x, F} T) = 1;

(forall y: F[x <- y] => (prod_{x, F} T) = T[x <- y] + (prod_{x, F /\ x != y} T)).

The same remarks apply as for the definition of the sum quantifier.

Example

(prod_{1 <= i <= 0} i⁵) = 1;

(prod_{0 <= i <= 5} a_i) = a₀*a₁*a₂*a₃*a₄*a₅

(prod_{0 <= i <= 100} a_i) = a₀*a₁*a₂* (prod_{3 <= i <= 100} a_i)

(prod_{0 <= i <= 100} a_i) = (prod_{0 <= i <= 50} a_i) * (prod_{51 <= i <= 100} a_i)

(prod_{1 <= i <= 3, 1 <= j <= i} i+j) = (1+1)*(2+1)*(2+2)*(3+1)*(3+2)*(3+3).

We have the following identities.

Proposition 59 (Product Quantifier) For all variables i and j and formulas F (in which j does not occur freely), G (in which i does not occur freely), and H and terms T and U we have:

(prod_{i, F} (prod_{j, G} T)) = (prod_{j, G} (prod_{i, F} T)) = (prod_{i, j, F /\ G} T).

(prod_{i, F} T) * (prod_{i, H} T) = (prod_{i, F \/ H} T) * (prod_{i, F /\ H} T).

Furthermore, if term C is a term in which i does not occur freely, we have:

(prod_{i, F} C*T) = Cⁿ(prod_{i, F} T) (where n is the number of i for which F holds).

(prod_{i, F} C) = Cⁿ (where n is the number of i for which F holds)

With the help of the product quantifier we can now formulate the uniqueness of prime number composition stated in Section Natural Numbers.

Proposition 60 (Prime Number Factorization) For every natural number n != 0, there exists a unique prime number factorization:

forall n in N_>0: (exists p: pf(n, p) /\ (forall q: pf(n, q) => p=q)).

A prime number factorization of n is a sequence of pairs (p, e) ordered by the primes p such that n is the product of all p^e.

pf(n, p) : <=>

   p: N -> N×N /\

   (forall i in N: p(i)₀ is prime /\ p(i)₀ < p(i+1)₀) /\

   (exists k in N: n = (prod_{0 <= i <= k} p(i)₀^p(i)₁) /\ forall i > k: p(i)₁ = 0)

Example Because 300=2²*3¹*5², we have for 300 the prime number factorization

[<2, 2>, <3, 1>, <5, 2>, <7, 0>, <11, 0>, <13, 0>, ...].

Likewise, 1 has the prime number factorization

[<2, 0>, <3, 0>, <5, 0>, <7, 0>, <11, 0>, <13, 0>, ...].

Author: Wolfgang Schreiner
Last Modification: October 4, 1999

(forall x: ~F)	=>	(sum_{x, F} `T`) = 0;
(forall y: `F`[`x` <- `y`]	=>	(sum_{x, F} `T`) = `T`[`x` <- `y`] + (sum_{x, F /\ x != y} `T`)).

(forall x: ~F)	=>	(prod_{x, F} `T`) = 1;
(forall y: `F`[`x` <- `y`]	=>	(prod_{x, F} `T`) = `T`[`x` <- `y`] + (prod_{x, F /\ x != y} `T`)).