Return-Path: Delivery-Date: Received: from ted.cs.uidaho.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) outside ac.uk; Thu, 18 Feb 1993 11:55:47 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA26075; Thu, 18 Feb 93 03:25:11 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from moa.pmms.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA26070; Thu, 18 Feb 93 03:25:04 -0800 Received: by moa.pmms.cam.ac.uk (UK-Smail 3.1.25.1/1); Thu, 18 Feb 93 11:23 GMT Message-Id: Date: Thu, 18 Feb 93 11:23 GMT From: Thomas Forster To: R.B.Jones@uk.co.icl.wins.win0109, info-hol@edu.uidaho.cs.ted Subject: Re: Strength of HOL I haven't seen Kemeny's proof. It is alluded to in Quine's 1967 book on Set Theory. It could procede as follows. Prove the consistency of each finite fragment of type theory (the theory of only finitely many types) and then use a compactness argument to infer the consistency of the whole thing. Altho' the consistency of such fragments of type theory can be proved consistent in type theory the corresponding compactnes argument is not available because the proofs are not uniform. Thus type-thory is saved from being able to prove its own consistency by being $\omega$-incomplete. I am cautious about extending this to theories like HOL because the effect of polymorphism on consistency strength is mysterious to me! tf