Go backward to 2.3.4 Quantified FormulasGo up to 2.3 Predicate Logic

### 2.3.5 Local Definitions

Apart from universal and existential quantification of formulas, there exist several other frequently occurring quantifiers, most notably quantifiers for introducing local definitions.

Proposition 17 (Local Definitions) Let x be a variable, T and S be terms, and A be a formula. Then the following are formulas with bound variable x:
 (let x = T: A) (A where x = T)
The following are terms:
 (let x = T: S) (S where x = T)
We omit the parentheses, if A, T, and S are unambiguous.

This definition shows that also terms (not only formulas) may be quantified.

Alternative Forms  Various syntactic forms express local definitions.

• Let x be T. Then we have A.
• Let x be T in A.
• A, where x=T.
• f(x) := Sx,y, where y=Tx;
• `let(x = T: A)`

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

Proposition 18 (Semantics of Local Definitions) Let x be a variable, A be a formula, and T and S be terms. Under a given assignment in a domain,
• the meaning of (let x = T: A) respectively that of (A where x = T) is the meaning of A in the extended assignment where x is mapped to the value of T;
• the meaning of (let x = T: S) respectively that of (S where x =T) is the value of S in the extended assignment where x is mapped to the value of T.

Thus both operators let and where are just different syntactic forms for the same concept.

Example  Take the domain of natural numbers and assignment [x |-> 1]. Then the proposition
let y = 0: x <= y
is false because 1 <= 0 does not hold.

The function f defined as

f(x) := s*x+s where s=x+1
has the same meaning as if it were defined as
f(x) := (x+1)*x+(x+1).

The last example shows that local definitions are just convenient forms for structuring formulas by giving names to values. We can always remove the quantifier by replacing any free occurrence of the quantified variable x by its defining term T.

Example  The formula
 x | y /\  exists z: y | z where y=2x
is equivalent to
x | 2x /\  exists z: 2x | z
Likewise, the formula
 x | y /\  exists y: y | x where y=2x
is equivalent to
x | 2x /\  exists y: y | x
However, it is not equivalent to
x | 2x /\  exists y: 2x | x
because the second occurrence of y is within the scope of another quantifier that binds this variable.

Actually, local definitions can be replaced by existential respectively universal quantifiers.

Proposition 19 (Replacement of Local Definitions) Let x be a variable, T be a term, and A be a formula. Then we have
 (let x = T: A) iff (forall x = T: A) (let x = T: A) iff (exists x = T: A)

The universal/existential formulas in above proposition are the previously introduced shortcuts for (forall x: x = T => A) and (exists x: x = T /\  A). The proposition is true, because for every term T there exists exactly one x such that x = T.

In the Logic Evaluator, local definitions are implemented for formulas as well as for terms as shown below:

Operational Interpretation  A term with a local definition is implemented in the evaluator by an object of the following Java class:

```public final class LetTerm implements Term
{
private String variable;
private Term term;
private Term body;

public LetTerm(String _variable, Term _term, Term _body)
{
variable = _variable;
term = _term;
body = _body;
}

public Value eval() throws EvalException
{
Context.begin(variable, term.eval());
Value result = body.eval();
Context.end();
return result;
}
}
```
The Java expression `new LetTerm(x, T, S)` thus evaluates to the meaning of let x=T: S. As one can see, we construct a new context in which x is bound to the value of T and evaluate S in this context.

Formulas with local definitions are implemented analogously.

Convention  We merge multiple local definitions, i.e., instead of writing (let x=1: let y=2: (x+y)*(x-y)), we usually write

let x=1, y=2: (x+y)*(x-y)
or correspondingly
(x+y)*(x-y) where x=1, y=2
Also the Logic Evaluator implements local definitions
```let(x_0 = T_0, ..., x_n-1 = T_n-1: A)
```
with any number of quantified variables.
Author: Wolfgang Schreiner
Last Modification: October 4, 1999