Return-Path: <john.harrison-request@uk.ac.cam.cl>
Delivery-Date: 
Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.4) outside ac.uk; Fri, 12 Feb 1993 14:15:18 +0000
Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28155;
          Fri, 12 Feb 93 06:00:07 -0800
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
Received: from life.ai.mit.edu by ted.cs.uidaho.edu (16.6/1.34) id AA28150;
          Fri, 12 Feb 93 06:00:00 -0800
Received: from spock (spock.ai.mit.edu) by life.ai.mit.edu (4.1/AI-4.10) 
          id AA23172; Fri, 12 Feb 93 08:59:07 EST
From: dam@edu.mit.ai (David McAllester)
Received: by spock (4.1/AI-4.10) id AA09636; Fri, 12 Feb 93 08:59:50 EST
Date: Fri, 12 Feb 93 08:59:50 EST
Message-Id: <9302121359.AA09636@spock>
To: John.Harrison@uk.ac.cam.cl
Cc: info-hol@edu.uidaho.cs.ted
Cc: chen@edu.cornell.cs
In-Reply-To: John Harrison's message of Fri, 12 Feb 93 11:01:35 +0000 <"swan.cl.ca.415:12.02.93.11.01.42"@cl.cam.ac.uk>
Subject: power of HOL

I am not an expert on HOL but it seems likely that "Jone's Conjecture"
that every recursive function is higher order primitive recursive is
false.  The set of recursive functions is not RE.  This means that one
can not construct a procedure that prints an infinite list of programs
such that every recursive function is computed by some program in the
list.  If one could construct such a list then one could construct a
recursive function that "diagonalized" over the functions on the list
and hence was different from each of them.  Since the higher order
primitive recursive functions can be enumerated, they can not include
all recursive functions.  To include all recursive functions one must
also include some partial functions.  For any sound (RE) proof system
there must exist recursive functions that can not be proven to be
recursive (the functions that are provably recursive can be
enumerated).

	David McAllester