Return-Path: 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, 28 Jun 1995 18:47:42 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA001549429; Wed, 28 Jun 1995 11:10:29 -0600 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from irafs1.ira.uka.de by leopard.cs.byu.edu with SMTP (1.37.109.15/16.2) id AA298919400; Wed, 28 Jun 1995 11:10:00 -0600 Received: from ira.uka.de (actually i80s35) by irafs1 with SMTP (PP); Wed, 28 Jun 1995 19:09:27 +0200 To: info-hol@leopard.cs.byu.edu Subject: Semantics of HOL Date: Wed, 28 Jun 1995 19:07:18 +0200 From: schneide Message-Id: <"irafs1.ira.080:28.06.95.17.09.31"@ira.uka.de> John explained the difference of the semantics of typed lambda calculi and the semantics of HOL. In essence, typed lambda calculi can be simulated in first order logic, while the HOL formulae can only be simulated in first order logic if we assume (nonstandard) Henkin interpretations. By the way, Kerber investigated for such translations of HOL into first-order logic and used a first-order theorem prover to automatically prove higher-order theorems. Of course, his approach is complete only for the general interpretations. However, it can be used to detect nontheorems quickly, since each standard theorem is a also a nonstandard theorem. Hence, there is a significant difference, between typed lambda calculi and the corresponding subset of formulae of HOL. I was not aware of this. Klaus.