Go backward to 2.3.3 EqualityGo up to 2.3 Predicate LogicGo forward to 2.3.5 Local Definitions |

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.

**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`)

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.

**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.

is to be interpreted asforallx:p(x) =>existsy:q(f(x),y)

and not as (forallx: (p(x) =>existsy:q(f(x),y)).

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

0 <= 0, 0 <= 1, 0 <= 2, ...Likewise, the existential formula

3 | 15.

In the domain of integer numbers withforallx:a(x) =>b(x,f(x)).

Every non-negative integer number is less than or equal its square.In the domain of character strings with

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

is the same as the meaning offorallx:existsy:x*y<=z

but it isforally:existsw:y*w<=z

(because a free variable must not be renamed).forallx:existsy:x*y<=w.

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

is true, if the current assignment maps the free variableforally:x<=y

is trueexistsx:forally:x<=y

could be also written asforallx:forally:x<=x+y

We recommend to always write all quantifiers to avoid misinterpretations.x<=x+y.

We will sometimes use the following notation.

the phrase we get fromP[x<-T]

F[x<- 1] =p(1) /\r(1,y) /\forallx:p(x)

**Patterns** A frequently occuring formula pattern is
**forall** `x`: `A`_{x} => `B`
where `A`_{x} is a formula with free variable `x`. Such a
formula is often written as

provided that the quantified variableforallA_{x}:B

existsA_{x}:B.

- The formula
**forall**`x`:**exists**0 <=`y`<=`x`: |`x`- 2*`y`| <= 1**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:

The Java expressionpublic 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; } }

`(new Forall(``x`, `d`, `A`)).eval()

computes the truth value of Likewise, we have the following implementation of existential quantification:

To compute the value of the expressionpublic 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; } }

`(new Exists(``x`,
`d`, `A`)).eval()

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

and instead of writingforallx,y:A

existsx,y:A.

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

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

**Duality**
Existential and universal quantification are dual concepts:

In other words, "not all

~ forallx:Aiff existsx: ~A~ existsx:Aiff forallx: ~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