Go backward to A.3 Explicit Function DefinitionsGo up to A Defining New NotionsGo forward to A.5 Recursive Definitions |

Letf(x_{0}, ...,x_{n-1}) be aysuch thatF.

However, this is just another way of writing an explicit definition

where (f(x_{0}, ...,x_{n-1}) :=suchy:F

(is a term with bound variablesuchx:F)

The value of this term is some `x` such that `F` holds (if such an
`x` exists). We omit the parentheses if `F` is clear.

Frequently, we write

to denotesuchxinS:F

**Reasoning**
When reasoning about implicitly defined objects with have to take special care
because the definition may be inconsistent (i.e., no object with the denoted
property exists) or not unique (multiple objects satisfy the property).

All that we actually have is the knowledge

i.e., if an object with property

( existsx:F) => (forallx:x= (suchx:F) =>F),

Consequently, we have for a function definition

the knowledgef(x_{0}, ...,x_{n-1}) :=suchy:F

i.e., for any tuple of function arguments the result value satisfies

( forallx_{0}, ...,x_{n-1}: (existsy:F) => (forally:y=f(x_{0}, ...,x_{n-1}) =>F)),

Therefore, for given `x`_{0}, ..., `x`_{n-1}, we first
have to prove

before we may assume that, for everyexistsy:F.

Then 12/4 = 3 because 3*4 = 12.x/y:=suchq:q*y=x.

Take a := 1/0. We must *not* assume that a*0 = 1,
because we cannot prove **exists** `q`: `q`*0 = 1.

**Such Terms and Predicates**
An alternative to defining a function

is always to define a predicate

f(x) :=suchy:F

Apparently, we then have the relationship

p(x,y) : <=>F.

However, it may be easier to understand (and to reason about) statements that are formulated with the help of the predicate than with the corresponding "such" term: for every formula

f(x) :=suchy:p(x,y).

is equivalent to

G[y<-f(x)]

which may be preferrable in some situations.

( forally:p(x,y) =>G)

We then wish to state that, for all sequences

lim( s) :=sucha:sconverges toa.

where, for every

lim( s+t) = lim(s)+lim(t)

Inserting the definition of "lim" gives us the statement

which is rather difficult to prove.

( sucha:s+tconverges toa) =( suchb:sconverges tob) + (suchc:tconverges toc)

However, above statement can be also formulated as

which is much more amenable to a formal proof.

foralla,b,c:( s+tconverges toa/\sconverges tob/\tconverges toc) =>a=b+c.

As the previous example shows, it may be advisable to "switch" from the formulation of a statement with "such terms" to a statement with corresponding predicates to understand the subtleties of the statement.

**Logic Evaluator**
We have a restricted form of the "such" quantifier that allows to express
the value of the
term (**such** `x` in `S`: `F`) as

In general, the quantifier binds multiple variablessuch(xinS:F,x)

The value of this term can be expressed by the standard quantifier assuch(x_0 in~T_0, ...,x_n-1 in~T_n-1:F,T)

where

( lett=suchtthat( existsx_{0}inT_{0}, ...,x_{n-1}inT_{n-1}:t=<x_{0}, ...,x_{n-1}> /\F)x_{0}=t_{0},... x_{n-1}=t_{n-1}:T)

**Operational Interpretation** A `such`

expression is an
instance of the Java class shown below.

public final class SuchThat implements Term { private String variable; private Term domain; private Formula formula; private Term term; public SuchThat(String _variable, Term _domain, Formula _formula, Term _term) { variable = _variable; domain = _domain; formula = _formula; term = _term; } public Value eval() throws EvalException { Iterator iterator = Model.iterator(domain); while (iterator.hasNext()) { Value result = null; Context.begin(variable, iterator.next()); if (formula.eval()) result = term.eval(); Context.end(); if (result != null) return result; } throw new EvalException("no such value"); } }

The Java expression `(new SuchThat(`

computes the value of `x`, `d`, `F`,
`T`)).eval()**let** `x` = (**such** `x`
in `d`: `F`): `T`. 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 `F`. If the formula
is true, we evaluate `T` and return its value.

**Unique Implicit Function Definitions**
The "such quanifier" does not necessarily determine a unique value,
consequently an implicit function definition not always determines a function
uniquely.

Letor, in other words,f(x) be aysuch thaty|x.

where | denotes the predicate "divides". Then all we know is thatf(x) :=suchy:y|x

Frequently, however an implicit definition is given in the form

letwhich implies that there exists at most onef(x_{0}, ...,x_{n-1}) betheysuch thatF

This is equivalent to stating, in addition to

also the condition (which has to be proved)

f(x_{0}, ...,x_{n-1}) :=suchy:F,

( forallx_{0}, ...,x_{n-1},y:F=>y=f(x_{0}, ...,x_{n-1})).

Letbecause from 6|12 we must not conclude f(12) = 6.f(x) be theysuch thaty|x.

However, we may define

LetSince 3*4=12, we may conclude 12/4 = 3.x/ybe theqsuch thatq*y=x.

Author: Wolfgang Schreiner

Last Modification: October 4, 1999