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

```magma
> 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(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.

```magma
> 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

```