Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
X400-Received: by mta eros.uknet.ac.uk in /PRMD=UK.AC/ADMD=GOLD 400/C=GB/;
               Relayed; Fri, 15 May 1992 17:53:24 +0100
X400-Received: by /PRMD=icl/ADMD=gold 400/C=GB/; converted (ia5); Relayed;
               Fri, 15 May 1992 17:35:41 +0100
Date: Fri, 15 May 1992 17:35:41 +0100
X400-Originator: R.B.Jones@uucp.win0109
X400-Mts-Identifier: [/PRMD=icl/ADMD=gold 400/C=GB/;win0109 0000012600001491]
Original-Encoded-Information-Types: ia5, undefined
X400-Content-Type: P2-1984 (2)
Content-Identifier: 1491
From: R.B.Jones@uucp.win0109
Message-Id: <"1491*/I=RB/S=Jones/OU=win0109/O=icl/PRMD=icl/ADMD=gold 400/C=GB/"@MHS>
To: info-hol@edu.uidaho.cs.ted
Subject: definability of functions in HOL


------------------------------ Start of body part 1

It is not safe to conclude anything about what functions can be
defined or proven total in HOL from considerations of the HOL
type system, since HOL does not obtain its logical strength from
the type system.  If this were safe we would have to conclude
that Zermelo Fraenkel is a weak system because it has no type
system at all.

------------------------------ Start of body part 2


Logically, HOL is similar in strength to Zermelo set theory, and can therefore
define and prove total any function which is provably total in Zermelo set
theory.

Without any change to the type system of HOL, by adding extra axioms it is
easy to increase the logical strength of the system to that of Zermelo Fraenkel
set theory or beyond.  The set of functions which can be proven total is then
extended.

Roger Jones
International Computers Limited
R.B.Jones@win0109.wins.icl.co.uk

------------------------------ End of body part 2