Prev Up Next
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

Prev Up Next