(1) Explicitly via the choice operator @ (an indefinite descriptor, so "@x.
P[x]" means "some x such that P[x]"). For example, one could define
inv = \x. @y. x * y = 1
(2) Via the principle of constant specification, which allows the
introduction of constants when a witness can be shown to exist.
For example:
|- !x. ~(x = 0) ==> ?y. x * y = 1
so
|- !x. ?y. ~(x = 0) ==> (x * y = 1)
Skolemizing
|- ?f. !x. ~(x = 0) ==> (x * f(x) = 1)
and introducing a constant "inv":
|- !x. ~(x = 0) ==> (x * inv(x) = 1)
Sometimes (1) results in more accidental theorems. We can't say much about
inv(0), but we do at least know that it's "@y. F" (F = falsum). This means that
any other constant of the same type defined in a similar way will also be equal
to "@y. F" when the body is false. Method (2) does not have this weakness. In
fact one could define two constants "inv" and "inv'" based on the same theorem,
without any relationship between inv(0) and inv'(0) being deducible. Some
HOL users considered this sufficiently important to justify the principle of
constant specification (in the old days, HOL only allowed definitions of the
direct form "c = <closed term>", or so I'm told). On the other hand, we are not
explicit about the value of "@y. F" in a model. In the standard HOL semantics,
we just assume a single choice function from the start. You can read this
semantics (due to Andy Pitts) in the HOL book from CUP, or in machine-readable
form in the standard HOL distribution.
John.