Full-Name: Joshua D. Guttman
Posted-Date: Thu, 25 Jul 91 14:55:28 -0400
Date: Thu, 25 Jul 91 14:55:28 -0400
From: guttman@org.mitre.linus
Message-Id: <9107251855.AA12153@malabar.mitre.org>
To: info-hol@edu.uidaho.cs.ted
Subject: Semantics of select
In-Reply-To: Sandy Murphy's message of Tue, 23 Jul 1991 22:16:40 GMT
Postal-Address: MITRE, Mail Stop A156 \\ Burlington Rd. \\ Bedford, MA 01730

I've always found the select operator (i.e. Hilbert's epsilon) unappealing
because its semantics is "non-deterministic".  That is, without it, we have the
property that the truth condition for a formula is completely determined by the
meanings of its parts, given the syntactic way it is put together out of the
parts.

For instance, if we have a traditional Tarski-style model-theoretic semantics,
then the denotation of a compound at a variable assignment is completely
determined by the denotations of its components at variable assignments
(possibly a set of assignments is relevant).  The same idea can also be worked
out in other ways than the Tarskian one.  My personal view is that the idea can
be the basis of a general characterization of logical constants and inferences.

However, this property disappears if epsilon is included, since the denotation
of an epsilon term (even if it has no free variables) is not determined by the
meaning of its body.  If a logic can accomodate undefined expressions, a
definite descriptor operator is much better, because it has a denotation just
in case a unique denotation is determined.

The fact that the model can be enriched by adding a well-ordering of the
objects doesn't really calm my worry.  After all, the language gives us no
access to this well-ordering.  Hence, as far as what we can do in the language
is concerned, epsilon terms don't behave like "normal" terms.

So I wonder whether Sandy Murphy's troubles with epsilon arise from this
anomaly in the semantics.  And I'd like to ask:  Why does HOL have to have this
operator, and how is it properly (reliably) used?

        Josh

PS-- History/motivation of epsilon.  My understanding is that Hilbert (or, more
likely, Bernays) invented this operator as a "technical trick", because they
found proof-theoretic analysis easier with epsilon-terms than with existential
quantifiers.  Bill Tait's view is that this is no longer the case, as the
infinitary cut-elimination theorem provides a more convenient method.  Was
there ever any more semantic motivation for using epsilon terms in logic?