Go backward to 8 \-abstraction
Go up to Top
Go forward to 10 Signature morphisms
9 Description operator
A description operator allows to talk about the
value satisfying a given property/formula.
The description operator is also called Hilbert
operator in total frameworks, where it selects an
arbitrary value. Due to the presence of partiality,
we can adopt the more satisfactory solution,
which -unlike the Hilbert operator- is a true
conservative extension:
the description operator is
undefined for properties that do not hold for
exactly one value [Far91].
A consequence of introducing the description operator
is that terms and formulae have to be defined
inductively in parallel.
In presence of \-abstraction, a description operator
can be defined as follows:
|
op Delta: (t => truth) --> t |
| axiom Delta(P) = e x <=> exist ! y:t.(P(y) /\ y=x) |
|
Then Delta(\x:t.phi) selects the value
for which phi holds (if there is a unique one).
Therefore, a description operator need not be
included in the language.
CoFI
Note: L-8 ---- 7 January 1998.
Comments to till@informatik.uni-bremen.de