Go backward to 2.3.4 Quantified FormulasGo up to 2.3 Predicate Logic |

The following are terms:

( letx=T:A)( Awherex=T)

We omit the parentheses, if

( letx=T:S)( Swherex=T)

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`) :=`S`_{x,y}, where`y`=`T`_{x};`let(`

`x`=`T`:`A`)

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

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

is false because 1 <= 0 does not hold.lety= 0:x<=y

The function `f` defined as

has the same meaning as if it were defined asf(x) :=s*x+swheres=x+1

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

is equivalent to

x|y/\existsz:y|zwherey=2x

Likewise, the formulax| 2x/\existsz: 2x|z

is equivalent to

x|y/\existsy:y|xwherey=2x

However,x| 2x/\existsy:y|x

because the second occurrence ofx| 2x/\existsy: 2x|x

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

( letx=T:A)iff ( forallx=T:A)( letx=T:A)iff ( existsx=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:

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

`new LetTerm(``x`, `T`, `S`)

thus
evaluates to the meaning of 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

or correspondinglyletx=1,y=2: (x+y)*(x-y)

(Also the Logic Evaluator implements local definitionsx+y)*(x-y)wherex=1,y=2

with any number of quantified variables.let(x_0 =T_0, ...,x_n-1 =T_n-1:A)

Author: Wolfgang Schreiner

Last Modification: October 4, 1999