   Go up to 4.7 Arithmetic NotionsGo forward to 4.7.2 Arithmetic Quantifiers ### 4.7.1 Minimum and Maximum

Definition 54 (Minimum and Maximum Quantifier) If x is a variable and F is a formula, then the following are terms with bound variable x:
 minx F; maxx F.
The value of the first term is the smallest value of x such that F holds; the value of the second term is the largest such value, i.e.,
 minx F := such x: F /\  (forall y: F[x <- y] => x <= y); maxx F := such x: F /\  (forall y: F[x <- y] => x >= y).

Usually the variable x is dropped and has to be deduced from the context.

We can use this notion to define corresponding functions on sets as follows.

Definition 55 (Minimum and Maximum Functions)
 min(S) := minx x in S; max(S) := maxx x in S;

Please note that the definition of "min" and "max" depends on the choice of the predicate <= . Furthermore, minimum and maximum are not necessarily defined.

Example
• We have
maxx (prime(x) /\  x | 100) = 5.
• The value of
min({1/x: x in N> 0})
is undefined because for every x in {1/1, 1/2, 1/3, 1/4, ...} there is always an y in this set with y < x, namely 1/(x+1).

Author: Wolfgang Schreiner
Last Modification: October 4, 1999   