[Next] [Prev] [Right] [Left] [Up] [Index] [Root]
Quantifiers

### 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 in 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_1, ..., t_r){ 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 t_1, ..., t_r 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.

P may be omitted if it is always true.

##### exists(t_1, ..., t_r){ e(x_1, ..., x_k) : x_1 in E_1, ..., x_k in E_k | P(x_1, ..., x_k) }
Given enumerated structures E_1, ..., E_k, and a Boolean expression P(x_1, ..., x_k), the Boolean value true is returned if there is an element <y_1, ..., y_k> in the Cartesian product E_1 x ... x E_k, such that P(y_1, ..., y_k) is true. If P(x_1, ..., x_k) is not true for any element (y_1, ..., y_k) of E_1 x ... x E_k, then the Boolean value false is returned.

Moreover, if P(x_1, ..., x_k) is found to be true for the element <y_1, ..., y_k> of E_1 x ... x E_k, then in the first form of the exists expression, the variable t will be assigned the value of the expression e(y_1, ..., y_k). If P(x_1, ..., x_k) is never true for an element of E_1 x ... x E_k, then the variable t will be left unassigned. In the second form, where r variables t_1, ..., t_r are given, the result e(y_1, ..., y_k) 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_1, ..., x_k) is never true. The clause (t) may be omitted entirely.

P may be omitted if it is always true.

If successive structures E_i and E_(i + 1) are identical, then the abbreviation x_i, x_(i + 1) in E_i may be used.

### Example Set_Exists (H4E11)

As a variation on an earlier example, we check whether or not some integers can be written as sums of cubes (less than 10^3 in absolute value):

```> print exists(t){ <x, y> : x, y in [ t^3 : t in [-10..10] ] | x + y eq 218 };
true
> print t;
<-125, 343>
> print exists(t){ <x, y> : x, y in [ t^3 : t in [1..10] ] | x + y eq 218 };
false
> print t;
>> print t;
^
User error: Identifier 't' has not been declared
```

##### forall(t_1, ..., t_r){ 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 t_1, ..., t_r 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.

P may be omitted if it is always true.

##### forall(t_1, ..., t_r){ e(x_1, ..., x_k) : x_1 in E_1, ..., x_
Given sets E_1, ..., E_k, and a Boolean expression P(x_1, ..., x_k), the Boolean value true is returned if P(x_1, ..., x_k) is true for every element (x_1, ..., x_k) in the Cartesian product E_1 x ... x E_k.

If P(x_1, ..., x_k) fails to be true for some element (y_1, ..., y_k) of E_1 x ... x E_k, then the Boolean value false is returned.

Moreover, if P(x_1, ..., x_k) is false for the element <y_1, ..., y_k> of E_1 x ... x E_k, then in the first form of the exists expression, the variable t will be assigned the value of the expression e(y_1, ..., y_k). If P(x_1, ..., x_k) is true for every element of E_1 x ... x E_k, then the variable t will be left unassigned. In the second form, where r variables t_1, ..., t_r are given, the result e(y_1, ..., y_k) 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_1, ..., x_k) is never true. The clause (t) may be omitted entirely.

P may be omitted if it is always true.

If successive structures E_i and E_(i + 1) are identical, then the abbreviation x_i, x_(i + 1) in E_i may be used.

### Example Set_NestedExists (H4E12)

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 epsilon (with |epsilon|leq1) is always a sum of squares.

```> print 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
> print u;
77
```

[Next] [Prev] [Right] [Left] [Up] [Index] [Root]