   Go backward to 2.3.3 EqualityGo up to 2.3 Predicate LogicGo forward to 2.3.5 Local Definitions ### 2.3.4 Quantified Formulas

In elementary terms and atomic formulas (applications of functions and predicates), the meaning of variables depends on a given assignment. We say that these variables are  free (frei) in the corresponding phrases. We now introduce a concept to give phrases with variables a meaning independently of any variable assignment.

Definition 18 (Quantifier) A  quantifier (Quantor) is a syntactic operator that combines a variable and a phrase to form a new phrase. The meaning of the new phrase does not depend on a given assignment to determine the value of the quantified variable; we say that this variable is  bound (gebunden) by the quantifier.

If every variable in a syntactic phrase is bound by a quantifier, the phrase is said to be  closed (geschlossen).

The meaning of a phrase does not depend on the name of the bound variable; we can replace this name by any other name without making a difference. Above definition implies that the meaning of a closed phrase does not depend on a given variable assignment but only on the considered domain.

In predicate logic, we have two important kinds of quantified formulas.

Proposition 15 (Quantified Formulas) If x is a variable and A is a formula then the following are formulas with bound variable x:
Universal Quantification
"for all x, A" ("für alle x, A")
(forall x: A)
Existential Quantification
"there exists x, A" ("es existiert x, A")
(exists x: A)
We omit the parentheses, if A is unambiguous.

When writing a quantified formula like (forall f: A) it is clear that any occurrence of f within A should denote a variable (not a constant). Consequently, we do not need to rely on any special convention for the names of quantified variables to distinguish them from function constants.

Alternative Forms  The formula forall x: A appears in various syntactic forms:

• forall x A
• /\x A;
• "for all x we have A" ("für alle x gilt A");
• "every x has A" ("jedes x hat die Eigenschaft A");
• "A, for all x" ("A gilt für alle x");
• `forall(x:A)`.

The last line denotes the input syntax of the Logic Evaluator.

Likewise, exists x: A may be expressed as:

• exists x A
• \/x A;
• "there exists x with A" ("es existiert ein x mit Eigenschaft A");
• "there is some x with A" ("es gibt ein x mit Eigenschaft A");
• "some x has A" ("ein x hat die Eigenschaft A");
• "A, for some x" ("A gilt für ein x").
• `exists(x:A)`.

Again, the last line is the input syntax of the Logic Evaluator.

Example  The following formulas are quantified:
• forall x: even(x) \/ odd(x);
• forall y: x <= y;
• "every x is non-negative"
forall x: ~(x < 0);
• "prime numbers exist"
exists x: isPrime(x).

The correct syntactic structure of formulas with nested quantifiers has to be often deduced from the free variables; parentheses should be used whenever necessary to resolve ambiguities.

Example  The formula
forall x: p(x) => exists y: q(f(x), y)
is to be interpreted as
forall x: (p(x) => exists y: q(f(x), y)).
and not as (forall x: p(x)) => exists y: q(f(x), y).

Definition 19 (Semantics of Quantified Formulas) Let x be a variable and A be a formula. The meaning of a quantified formula under an assignment in some domain is defined as follows:
• The formula forall x: A is true if and only if A is true for every value of x (i.e., A is true in every assignment extension where x is mapped to a value from the domain).
• The formula exists x: A is true if and only if A is true for some value of x (i.e., A is true in some assignment extension where x is mapped to a value from the domain).

Example  The universal formula forall x: y <= x is true in assignment [y |-> 0] over the domain of natural numbers with the usual interpretation of ` <= `, because 0 <= x is true for every natural number x:
0 <= 0, 0 <= 1, 0 <= 2, ...
Likewise, the existential formula exists x: x | 15 is true for every assignment over the natural numbers with `|' interpreted as `divides', because x | 15 is true for some natural number x (e.g. for 3):
3 | 15.

Example  Take the formula
forall x: a(x) => b(x, f(x)).
In the domain of integer numbers with a interpreted as "is non-negative", f interpreted as "square of" and b interpreted as "is less than or equal", the formula expresses the (true) statement
Every non-negative integer number is less than or equal its square.
In the domain of character strings with a interpreted as "is non-empty", f interpreted as "string without first character" and b interpreted as "is longer than", the formula expresses the (true) statement
Every non-empty character string is longer than the string without the first character.

Free and Bound Variables  As said above, the meaning of a formula does not depend on the name of a bound variable. For instance, the meaning of

forall x: exists y: x*y <= z
is the same as the meaning of
forall y: exists w: y*w <= z
but it is not the same as the meaning of
forall x: exists y: x*y <= w.
(because a free variable must not be renamed).

When stating a proposition, we usually operate with closed formulas, since their meaning is independent of any variable assignment. For instance, assume that we consider the domain of natural numbers with ` <= ' interpreted as usual. The statement

forall y: x <= y
is true, if the current assignment maps the free variable x to 0, and false, otherwise. On the contrary, the closed formula
exists x: forall y: x <= y
is true independently of the variable assignment. Sometimes, it is assumed that all free variables in a formula are universally quantified such that a formula
forall x: forall y: x <= x+y
could be also written as
x <= x+y.
We recommend to always write all quantifiers to avoid misinterpretations.

We will sometimes use the following notation.

Definition 20 (Free Variable Substitution) For every syntactic phrase P, variable x, and term T we denote by
P[x <- T]
the phrase we get from P by replacing every free occurrence of x by T.

Example  Let F := p(x) /\  r(x, y) /\  forall x: p(x). Then
F[x <- 1] = p(1) /\  r(1, y) /\  forall x: p(x)

Patterns  A frequently occuring formula pattern is forall x: Ax => B where Ax is a formula with free variable x. Such a formula is often written as

forall Ax: B
provided that the quantified variable x is clear from the context. Another such pattern is exists x: Ax /\  B which is typically written as
exists Ax: B.

Example
• The formula
forall x: exists 0 <= y <= x: | x - 2*y | <= 1
is an abbreviation for the formula
forall x: (exists y: (0 <= y) /\  (y <= x) /\  (| x - 2*y | <= 1)).
• The natural language sentence
"All Ferraris are red"
is an abbreviation for the sentence
"It holds for all objects that, if the object is a Ferrari, then the object is red"
which is represented by the formula
forall x: isFerrari(x) => isRed(x).
• The natural language sentence
"Some Ferraris are black"
is an abbreviation for the sentence
"There exists an object such that the object is a Ferrari and the object is black"
which is represented by the formula
exists x: isFerrari(x) /\  isBlack(x).

The Logic Evaluator can evaluate quantified formulas that are input in prefix form; however, we have to denote the domain that we consider (which must be finite). In the following example, our domain is the range of natural numbers less than or equal 100.

We may however also explicitly set the domain for a quantified variable:

Operational Interpretation  Variables are implemented by the following Java class:

```public final class Variable implements Term
{
private String variable;

public Variable(String _variable)
{
variable = _variable;
}

public String name()
{
return variable;
}

public Value eval() throws EvalException
{
Value value = Context.get(variable);
if (value == null) throw
new EvalException("no variable " + variable + " in context");
return value;
}
}
```

As we can see, the value of a variable is just determined by the context (the current variable assignment). This context is, e.g. provided by a universally quantified formula as an instance of the following Java class:

```public final class ForAll implements Formula
{
private String variable;
private Term domain;
private Formula formula;

public ForAll(String _variable, Term _domain, Formula _formula)
{
variable = _variable;
domain = _domain;
formula = _formula;
}

public boolean eval() throws EvalException
{
Iterator iterator = Model.iterator(domain);
while (iterator.hasNext())
{
Context.begin(variable, iterator.next());
boolean result = formula.eval();
Context.end();
if (!result) return false;
}
return true;
}
}
```
The Java expression `(new Forall(x, d, A)).eval()` computes the truth value of forall x: A in domain d. As one can see, we iterate over d and establish new contexts in which x is assigned each value of the domain in turn. In each context, we evaluate A. Only if the result is true for every value, the overall result is true.

Likewise, we have the following implementation of existential quantification:

```public final class Exists implements Formula
{
private String variable;
private Term domain;
private Formula formula;

public Exists(String _variable, Term _domain, Formula _formula)
{
variable = _variable;
domain = _domain;
formula = _formula;
}

public boolean eval() throws EvalException
{
Iterator iterator = Model.iterator(domain);
while (iterator.hasNext())
{
Context.begin(variable, iterator.next());
boolean result = formula.eval();
Context.end();
if (result) return true;
}
return false;
}
}
```
To compute the value of the expression ```(new Exists(x, d, A)).eval()```, we iterate over d and establish all contexts in which A is evaluated. If we find some value for which this result is true, the overall result is true.

Convention  Multiple quantifiers of the same kind are often "merged", i.e., instead of writing forall x: forall y: A we often write

forall x, y: A
and instead of writing exists x: exists y: A we write
exists x, y: A.

The same is true for the Logic Evaluator where you can write

```forall(x_0, ..., x_n-1: A)
exists(x_0, ..., x_n-1: A)
```
with any number of quantified variables.

Duality  Existential and universal quantification are dual concepts:

Proposition 16 (De Morgan's Laws) For every variable x and formula A, we have
 ~forall x: A iff exists x: ~A ~exists x: A iff forall x: ~A
In other words, "not all x have A" means the same as "there exists some x such that not A" and "there does not exist an x with A" means the same as "for all x, not A".

From these laws, it follows that exists x: A means the same as ~forall x: ~A; therefore frequently existential quantification is defined just as a syntactic abbreviation in terms of universal quantification (or vice versa).

Author: Wolfgang Schreiner
Last Modification: October 4, 1999   