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){ e(x): x in E | P(x) }#
exists(t₁, ..., tᵣ){ 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, \ldots, 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. The expression \(P\) may be omitted if it is always true.

exists(t){ e(x₁, ..., xₖ): x₁ in E₁, ..., xₖ in Eₖ | P(x₁, ..., xₖ)}#
exists(t₁, ..., tᵣ){ e(x₁, ..., xₖ) : x₁ in E₁, ..., xₖ in Eₖ | P }#: Given enumerated structures \(E_1, \ldots, E_k\), and a Boolean expression \(P(x_1\), \(\ldots\), \(x_k)\), the Boolean value true is returned if there is an element \(<y_1\), \(\ldots\), \(y_k>\) in the Cartesian product \(E_1 \times \cdots \times E_k\), such that \(P(y_1, \ldots, y_k)\) is true. If \(P(x_1, \ldots, x_k)\) is not true for any element \((y_1\), \(\ldots\), \(y_k)\) of \(E_1 \times \cdots \times E_k\), then the Boolean value false is returned. Moreover, if \(P(x_1\), \(\ldots\), \(x_k)\) is found to be true for the element \(<y_1, \ldots, y_k>\) of \(E_1 \times \cdots \times 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, \cdots, y_k)\). If \(P(x_1\), \(\ldots\), \(x_k)\) is never true for an element of \(E_1 \times \cdots \times E_k\), then the variable \(t\) will be left unassigned. In the second form, where \(r\) variables \(t_1, \ldots, t_r\) are given, the result \(e(y_1, \cdots, 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\), \(\ldots\), \(x_k)\) is never true. The clause (t) may be omitted entirely. The expression \(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: Exists (ex-eb9af3)#

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):

> 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

Run in calculator

forall(t){ e(x) : x in E | P(x) }#
forall(t₁, ..., tᵣ){ 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, \ldots, 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. The expression \(P\) may be omitted if it is always true.

forall(t){ e(x₁, ..., xₖ): x₁ in E₁, ..., xₖ in Eₖ | P(x₁, ..., xₖ)}#
forall(t₁, ..., tᵣ){ e(x₁, ..., xₖ) : x₁ in E₁, ..., xₖ in Eₖ | P }#: Given sets \(E_1, \ldots, E_k\), and a Boolean expression \(P(x_1\), \(\ldots\), \(x_k)\), the Boolean value true is returned if \(P(x_1, \ldots, x_k)\) is true for every element \((x_1\), \(\ldots\), \(x_k)\) in the Cartesian product \(E_1 \times \cdots \times E_k\). If \(P(x_1, \ldots, x_k)\) fails to be true for some element \((y_1\), \(\ldots\), \(y_k)\) of \(E_1 \times \cdots \times E_k\), then the Boolean value false is returned. Moreover, if \(P(x_1\), \(\ldots\), \(x_k)\) is false for the element \(<y_1, \ldots, y_k>\) of \(E_1 \times \cdots \times 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, \cdots, y_k)\). If \(P(x_1\), \(\ldots\), \(x_k)\) is true for every element of \(E_1 \times \cdots \times E_k\), then the variable \(t\) will be left unassigned. In the second form, where \(r\) variables \(t_1, \ldots, t_r\) are given, the result \(e(y_1, \cdots, 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\), \(\ldots\), \(x_k)\) is never true. The clause (t) may be omitted entirely. The expression \(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: Nested Exists (ex-8bbcd9)#

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\pm\epsilon\) (with \(|\epsilon|\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

Run in calculator