Go backward to 2.3.3 Equality Go up to 2.3 Predicate Logic Go forward to 2.3.5 Local Definitions

2.3.4 Quantified Formulas

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.

forall x: p(x) => exists y: q(f(x), y)

forall x: (p(x) => exists y: 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, ...

3 | 15.

forall x: a(x) => b(x, f(x)).

Every non-negative integer number is less than or equal its square.

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

forall y: exists w: y*w <= z

forall x: exists y: 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

forall y: x <= y

exists x: forall y: x <= y

forall x: forall y: x <= x+y

x <= x+y.

We will sometimes use the following notation.

P[x <- T]

F[x <- 1] = p(1) /\  r(1, y) /\  forall x: 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

forall A_x: B

exists A_x: B.

• 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;
  }
}

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;
  }
}

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

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) 

Duality  Existential and universal quantification are dual concepts:

~forall x: A	iff	exists x: ~A
~exists x: A	iff	forall x: ~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).