Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
X400-Received: by mta relay.pipex.net in /PRMD=pipex/ADMD=cwmail/C=GB/; Relayed;
               Fri, 12 Feb 1993 16:59:34 +0000
X400-Received: by /PRMD=icl/ADMD=gold 400/C=GB/; converted (ia5 text (2));
               Relayed; Fri, 12 Feb 1993 16:54:07 +0000
Date: Fri, 12 Feb 1993 16:54:07 +0000
X400-Originator: R.B.Jones@uk.co.icl.wins.win0109
X400-Recipients: info-hol@edu.uidaho.cs.ted
X400-Mts-Identifier: [/PRMD=icl/ADMD=gold 400/C=GB/;win0109 0000012600002261]
Original-Encoded-Information-Types: undefined (0)
X400-Content-Type: P2-1984 (2)
Content-Identifier: 2261
From: R.B.Jones@uk.co.icl.wins.win0109
Message-Id: <"2261*/I=RB/S=Jones/OU=win0109/O=icl/PRMD=icl/ADMD=gold 400/C=GB/"@MHS>
To: info-hol@edu.uidaho.cs.ted
Subject: Z/HOL/ProofPower


         Z is based on Zermelo set theory, not Zermelo-Fraenkel (so the 
         large sets aren't a problem Tom).  However the "tarting it up" 
         includes imposing a type system, which makes it more like HOL than 
         untyped set theory from some points of view.
         
         Its not clear from the literature what an acceptable logical 
         framework for Z is because of two conflicting positions:
         
              1.   Z specifications admit introducing arbitrary axiomatic 
                   extentions, with no requirement that they be 
                   conservative.  (so you could add the axiom of 
                   replacement if you could express it in Z)
         
              2.   On the other hand, Mike Spivey in some of his works has 
                   taken exception to the axiom of choice, so he appears to 
                   think that Z should be considered to be a bit like 
                   Zermelo set theory without the axiom of choice.
         
         In all consistent proof systems for Z there will be true facts 
         about specifications in Z which cannot be proven (because 
         arithmetic is incompletely formalisable) so ProofPower Z has this 
         property also.  However ProofPower has an axiom of choice in it, 
         so ProofPower Z is probably able to prove more facts than Mike 
         Spivey might think it should (though we believe this excludes 
         "false").
         
         As in accepted usage of Z, you can introduce arbitrary axiomatic 
         constraints in ProofPower Z, though ProofPower does provide basic 
         support for treating axiomatic descriptions as conservative 
         extensions.  In any case ProofPower will keep track of all the 
         non-conservative axioms you have introduced so at least you know 
         where you stand (and there is no mk_thm).
         
         Roger Jones
         International Computers Limited
         R.B.Jones@win0109.wins.icl.co.uk