Full-Name: Joshua D. Guttman
Posted-Date: Thu, 15 Aug 91 11:45:14 -0400
Date: Thu, 15 Aug 91 11:45:14 -0400
From: guttman@org.mitre.linus
Message-Id: <9108151545.AA02319@malabar.mitre.org>
To: info-hol@edu.uidaho.cs.ted
Cc: ian@com.oracorp.cambridge (Ian Sutherland)
In-Reply-To: ian@cambridge.oracorp.com's message of Wed, 14 Aug 1991 14:21:56 GM
Subject: Re: Choice
Postal-Address: MITRE, Mail Stop A156 \\ Burlington Rd. \\ Bedford, MA 01730

Ian,

Yes, I take it that your definition \x:(*->bool).(@y.(x y)) for the choice fn
should work just fine, and I used your expression for the ordering in one of my
later messages.

My main point was not that you can't (at all) get your hands on the meaning of
@ within the language (though I did carelessly put it that way).  Rather, the
idea was that if @ is construed as a part of the logic, then a structure for
*the signature of the language* doesn't determine the denotation of a term
using it.  Thus, its semantics are not compositionally determined without some
further information.  (Naturally, by contrast, the underlying sets *are*
determined, once we have been given a structure for that signature.)

Thus, @ is not like a genuine logical constant.

So I've come to the conclusion that @ should be considered as a *non-logical*
constant.  It just happens to be present in every signature of interest to the
HOL user.  It has polymorphic type:

  @:((* -> bool) -> *)

and it is governed by the non-logical axiom:

!f: * -> bool . (?x: * . f(x)) implies f(@(f))

The variable-binding syntax is just sugar.  With this approach, @ is part of
the signature of a particular formal language, rather than part of the logic.
So of course a structure for the signature of the language (on this view) will
explicitly assign a function as denotation to @.  The meaning of a term @(f) is
just the result of applying this function to the meaning of f.

        Josh

PS:  Ian-- I tried to send mail some time ago directly to
ian@cambridge.oracorp.com but I suspect it died along the way.  What's the
right address to use for you?