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; Fri, 12 Feb 1993 14:45:05 +0000 Received: by ted.cs.uidaho.edu (16.6/1.34) id AA28163; Fri, 12 Feb 93 06:31:59 -0800 Sender: info-hol-request@edu.uidaho.cs.ted Errors-To: info-hol-request@edu.uidaho.cs.ted Precedence: bulk Received: from swan.cl.cam.ac.uk by ted.cs.uidaho.edu (16.6/1.34) id AA28158; Fri, 12 Feb 93 06:31:51 -0800 Received: from razorbill.cl.cam.ac.uk (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.4) to cl; Fri, 12 Feb 1993 14:30:58 +0000 To: info-hol@edu.uidaho.cs.ted Subject: Z/ZF/Zermelo/ProofPower? Date: Fri, 12 Feb 93 14:30:52 +0000 From: Jim Grundy Message-Id: <"swan.cl.ca.057:12.02.93.14.31.17"@cl.cam.ac.uk> Here is a questions prompted by Thomas Forsters posting. I used to use Z (the specification langauge) lots. I was told by the people who taught it to me that Z was just tarted up ZF set theory (hence the name). This was a while back - before the new standardisation efforts and semantics for Z, but if this were still true... ICL have a tool for reasoning about Z specification built on top of their re-implementation of HOL. Now if ICL's HOL locic is essentially the same as the orginial HOL logic, which Thomas asserts is equivalent to Zermelo set theory, and as Thomas says there are theorems in ZF that are not theorems in Zermelo - does this mean that there are properties of Z specifications that can not be proved using the ICL tool? Jim