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 17:42:18 +0100
Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA15096;
          Wed, 25 May 1994 10:24:41 -0600
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Received: from dworshak.cs.uidaho.edu by leopard.cs.byu.edu 
          with SMTP (1.37.109.8/16.2) id AA15092;
          Wed, 25 May 1994 10:24:38 -0600
Received: from cornell.edu by dworshak.cs.uidaho.edu 
          with SMTP (1.37.109.8/16.2) id AA03736;
          Wed, 25 May 1994 09:24:40 -0700
Received: from msiadmin.cit.cornell.edu ([128.253.216.2]) by cornell.edu 
          with SMTP id <580187-6>; Wed, 25 May 1994 12:24:33 -0400
Date: Wed, 25 May 1994 12:24:13 -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 AA12325; Wed, 25 May 94 12:24:13 EDT
Message-Id: <9405251624.AA12325@msiadmin.cit.cornell.edu>
To: info-hol@cs.uidaho.edu, jug@itd.dsto.gov.au
Subject: Re: Class of automatic verifiable formulas
Cc: garrel@msiadmin.cit.cornell.edu

It is well known that higher order logic is undecidable.  Here are sketches
of two proofs of that result.

Proof sketch 1:  Higher order logic contains first order logic, and, as
Church proved in 1936, first order logic is undecidable.  Hence, higher order
logic is undecidable.

Proof sketch 2:  In higher order logic, Peano's axioms can be expressed by a
single formula.  Let P be such a formula.  If higher order logic were
decidable, it would be possible to decide, for arbitrary an arbitrary formla
A, whether P => A is a theorem of higher order logic.  But this would lead
to a decision procedure for Peano arithmetic, and no such procedure exists.

Tons of details must be filled in to turn the sketches into proofs, but
that can be done.

Regards,

Garrel