Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Wed, 25 May 1994 18:46:37 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA15919;
          Wed, 25 May 1994 11:34:25 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from cornell.edu by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) 
          id AA15915; Wed, 25 May 1994 11:34:23 -0600
Received: from msiadmin.cit.cornell.edu ([128.253.216.2]) by cornell.edu 
          with SMTP id <580308-1>; Wed, 25 May 1994 13:34:26 -0400
Date: Wed, 25 May 1994 13:34:09 -0400
From: garrel@msiadmin.cit.cornell.edu (Garrel Pottinger-MSI Visitor)
Received: from msipawn.409col_ave by msiadmin.cit.cornell.edu (4.1/1.5) 
          id AA12452; Wed, 25 May 94 13:34:09 EDT
Message-Id: <9405251734.AA12452@msiadmin.cit.cornell.edu>
To: info-hol@leopard.cs.byu.edu, schneide@ira.uka.de
Subject: Re: Decidability
Cc: garrel@msiadmin.cit.cornell.edu

I'm not sure what Klaus means by saying:

  ... there is no algorithm which could list all theorems of the logic.
  HOL means "higher order logic", not the calculus of the HOL system.

But here are some facts that may be relevant to what he has in mind.  Until
further notice, the system under discussion is Church's type theory.

As I pointed out in an earlier message, using higher order logic makes
it possible to write down the Peano axioms as a single formula, P.  If
we consider as models only those structures in which a type alpha -> beta
contains all the functions from alpha to beta, then it can be shown that
P is categorical --- if M_1 and M_2 are models of P, then M_1 and M_2 are
isomorphic.  (The core idea of the proof is due to Dedekind.)

It follows that, where A is a formula of arithmetic:  (1) A is a true
assertion about the natural numbers if, and only if, P => A is valid in the
class of models under discussion, and (2) A is a false assertion about the
natural numbers if, and only if, not P => A is valid in that class of models.

Now suppose that the set of formulas valid in the aforesaid class of
models were effectively enumerable.  Then it would be possible to decide
as follows whether an arbitrary arithmetic formula A is a true assertion
about the natural numbers:

  Start enumerating the valid formulas and wait for one of P => A and
  P => not A to turn up in the enumeration, as, by the above, one or
  the other must.  If P => A appears in the enumeration, then A is
  a true arithmetic assertion.  If P => not A appears in the enumeration,
  then A is a false arithmetic assertion.

But there is no decision procedure for arithmetic truth, so, contrary
to the supposition, there is no effective enumeration of the set of formulas
valid in the class of structures in which a type alpha -> beta contains all
the functions from alpha to beta.

In 1950, Henkin showed that by enlarging the class of models to include
structures in which some functions from alpha to beta are omitted from
the type alpha -> beta, it is possible to define a notion of validity
for which the completeness of Church's type theory can be proved (see
reference appended.)

A couple of years ago, I extended Henkin's result to cover the HOL logic and
reported this in a message to info-hol.  If enough people are interested,
I can resend the report.

Regards,

Garrel

**********************************************************************

@article{henkin:completeness,
         author = "Leon Henkin",
         title = "Completeness in the Theory of Types",
         journal = "Journal of Symbolic Logic",
         volume = 15,
         year = 1950,
         pages = "81--91"
}