Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
To: info-hol@leopard.cs.byu.edu
Subject: Re: Semantics of HOL
In-Reply-To: Your message of "Tue, 27 Jun 1995 11:47:28 +0200." <"irafs1.ira.130:27.06.95.09.49.35"@ira.uka.de>
Date: Tue, 27 Jun 1995 14:44:16 +0100
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:089520:950627134447"@cl.cam.ac.uk>


Klaus writes:

| In the chapter on the semantics of HOL in the HOL
| documentation, the type a -> b is defined to be
| the set of a l l functions from the set assigned
| to a to the set assigned to the type b.
|   However, in type frames the type a -> b is more
| generally defined to be the set of s o m e  functions
| from the set assigned to a to the set assigned to the
| type b (see e.g. Andrew's book). E.g. a and b assigned
| to cpos, this definition allows to assign a -> b the
| set of all continous functions which form a strict
| subset of the set of all functions (if a and b assigned
| to cpos).
|   In the HOL documentation it is stressed that the
| semantics is the set of all functions, but it is not
| mentioned (and also not clear to me) if this means a
| real restriction or not?

The standard semantics for higher order logic interprets a->b as the full
function space. Arguably it's this intended semantics that really makes the
logic "higher order".

By allowing arbitrary interpretations for notions like function
application, we can regard HOL as just a syntactically sugared first order
logic (where function application is just a 2-place function). With respect
to this broader class of interpretations, one can prove a completeness
theorem just as one can for first order logic. (That is, something is
provable iff it's true under all these interpretations.)

In fact Henkin showed that one can still get a completeness theorem with
just one disturbance of the standard semantics: allow interpretations
where a->b is a proper subset of the full function space (the usual jargon
is that these models are "general" rather than "full"). See Garrell
Pottinger's message to info-hol on 28 Jan 92 for a completeness theorem for
the HOL logic wrt these general models. Such a completeness theorem is out
of the question wrt standard models only, since the truths of arithmetic
are not recursively enumerable, but arithmetic truth reduces to higher order
validity because Peano's axioms are second order categorical.

I don't really see any practical applications for interpreting the function
space more generally -- I'm not quite sure what you have in mind. Perhaps
one could somehow use it to extract programs from proofs. For example, the
realizability interpretation of intuitionistic logic interprets logical
operations as constructions on recursive functions. Of course, some
classical theorems (notably the law of the excluded middle) do not in
general hold under such an interpretation.

John.