Quantifiers

To test whether some enumerated set is empty or not, one may use the IsEmpty function. However, to use IsEmpty, the set has to be created in full first. The existential quantifier exists enables one to do the test and abort the construction of the set as soon as an element is found; moreover, the element found will be assigned to a variable.

Likewise, forall enables one to abort the construction of the set as soon as an element not satisfying a certain property is encountered.

Note that exists(t){ e(x) : x in E | P(x) } is not designed to return true if an element of the set of values e(x) satisfies P, but rather if there is an x∈E satisfying P(x) (in which case e(x) is assigned to t).

For the notation used here, see the beginning of this chapter.

exists(t){ e(x): x in E | P(x) }
exists(t1, ..., tr){ e(x) :x in E | P(x) }
Given an enumerated structure E and a Boolean expression P(x), the Boolean value true is returned if E contains at least one element x for which P(x) is true. If P(x) is not true for any element x of E, then the Boolean value false is returned.

Moreover, if P(x) is found to be true for the element y, say, of E, then in the first form of the exists expression, variable t will be assigned the value of the expression e(y). If P(x) is never true for an element of E, t will be left unassigned. In the second form, where r variables t1, ..., tr are given, the result e(y) should be a tuple of length r; each variable will then be assigned to the corresponding component of the tuple. Similarly, all the variables will be left unassigned if P(x) is never true. The clause (t) may be omitted entirely.

The expression P may be omitted if it is always true.

exists(t){ e(x1, ..., xk): x1 in E1,..., xk in Ek | P(x1, ..., xk) }
exists(t1, ..., tr){ e(x1, ..., xk) :x1 in E1, ..., xk in Ek | P }
Given enumerated structures E1, ..., Ek, and a Boolean expression P(x1, ..., xk), the Boolean value true is returned if there is an element <y1, ..., yk> in the Cartesian product E1 x ... x Ek, such that P(y1, ..., yk) is true. If P(x1, ..., xk) is not true for any element (y1, ..., yk) of E1 x ... x Ek, then the Boolean value false is returned.

Moreover, if P(x1, ..., xk) is found to be true for the element <y1, ..., yk> of E1 x ... x Ek, then in the first form of the exists expression, the variable t will be assigned the value of the expression e(y1, ..., yk). If P(x1, ..., xk) is never true for an element of E1 x ... x Ek, then the variable t will be left unassigned. In the second form, where r variables t1, ..., tr are given, the result e(y1, ..., yk) should be a tuple of length r; each variable will then be assigned to the corresponding component of the tuple. Similarly, all the variables will be left unassigned if P(x1, ..., xk) is never true. The clause (t) may be omitted entirely.

The expression P may be omitted if it is always true.

If successive structures Ei and Ei + 1 are identical, then the abbreviation xi, xi + 1 in Ei may be used.

Example Set_Exists (H10E12)

As a variation on an earlier example, we check whether or not some integers can be written as sums of cubes (less than 103 in absolute value): 
> exists(t){ <x, y> : x, y in [ t^3 : t in [-10..10] ] | x + y eq 218 };
true
> t;
<-125, 343>
> exists(t){ <x, y> : x, y in [ t^3 : t in [1..10] ] | x + y eq 218 };
false
> t;
>> t;
   ^
User error: Identifier 't' has not been declared
forall(t){ e(x) : x in E | P(x) }
forall(t1, ..., tr){ e(x) :x in E | P(x) }
Given an enumerated structure E and a Boolean expression P(x), the Boolean value true is returned if P(x) is true for every element x of E.

If P(x) is not true for at least one element x of E, then the Boolean value false is returned.

Moreover, if P(x) is found to be false for the element y, say, of E, then in the first form of the exists expression, variable t will be assigned the value of the expression e(y). If P(x) is true for every element of E, t will be left unassigned. In the second form, where r variables t1, ..., tr are given, the result e(y) should be a tuple of length r; each variable will then be assigned to the corresponding component of the tuple. Similarly, all the variables will be left unassigned if P(x) is always true. The clause (t) may be omitted entirely.

The expression P may be omitted if it is always true.

forall(t){ e(x1, ..., xk): x1 in E1,..., xk in Ek | P(x1, ..., xk) }
forall(t1, ..., tr){ e(x1, ..., xk) :x1 in E1, ..., xk in Ek | P }
Given sets E1, ..., Ek, and a Boolean expression P(x1, ..., xk), the Boolean value true is returned if P(x1, ..., xk) is true for every element (x1, ..., xk) in the Cartesian product E1 x ... x Ek.

If P(x1, ..., xk) fails to be true for some element (y1, ..., yk) of E1 x ... x Ek, then the Boolean value false is returned.

Moreover, if P(x1, ..., xk) is false for the element <y1, ..., yk> of E1 x ... x Ek, then in the first form of the exists expression, the variable t will be assigned the value of the expression e(y1, ..., yk). If P(x1, ..., xk) is true for every element of E1 x ... x Ek, then the variable t will be left unassigned. In the second form, where r variables t1, ..., tr are given, the result e(y1, ..., yk) should be a tuple of length r; each variable will then be assigned to the corresponding component of the tuple. Similarly, all the variables will be left unassigned if P(x1, ..., xk) is never true. The clause (t) may be omitted entirely.

The expression P may be omitted if it is always true.

If successive structures Ei and Ei + 1 are identical, then the abbreviation xi, xi + 1 in Ei may be used.

Example Set_NestedExists (H10E13)

This example shows that forall and exists may be nested.

It is well known that every prime that is 1 modulo 4 can be written as the sum of two squares, but not every integer m congruent to 1 modulo 4 can. In this example we explore for small m whether perhaps m plus or minus ε (with |ε|leq1) is always a sum of squares. 

> forall(u){ m : m in [5..1000 by 4] |
>       exists{ <x, y, z> : x, y in [0..30], z in [-1, 0, 1] |
>          x^2+y^2+z eq m } };
false
> u;
77
V2.28, 13 July 2023