<html> <head> <meta http-equiv="content-type" content="text/html; charset=utf-8"> </head> <body text="#000000" bgcolor="#FFFFFF"> A good place to look for the low-down on the relationship between HOL and set theory is a paper by Thomas Forster written originally for (and published in the proceedings of) HUG94. "Weak systems of set theory related to HOL" This has however been subsequently augmented and corrected so it is better to go to Thomas Forster's web page <a class="moz-txt-link-freetext" href="https://www.dpmms.cam.ac.uk/~tf/">https://www.dpmms.cam.ac.uk/~tf/</a> or to write to him for a copy (tf at maths.cam.ac.uk). The essence of his conclusions as far as the present issue is concerned, (as I understand it) are as follows: HOL has the same consistency strength as Maclane Set theory, which is strictly weaker than Zermelo set theory. Therefore an embedding of Zemelo into HOL will not be possible without axiomatic extension of HOL, for which a strengthening of the axiom of infinity would suffice. For a typed Zermelo, and hence for the Z specification language the situation is different, and a full embedding of the Z specification language into HOL has been available in ProofPower since about 1994. What I address here is what is generally called a "shallow semantic embedding" or any embedding method which one would expect to be constrained by relative consistency strength. For a "deep" semantic embedding the constraints are more strict and a deep embedding of the Z specification language would also fail (without axiomatic extension). The question of "embedding a proof in Z" might be interpreted in a way not subject to such constraints, since the notion of proof in Z (as opposed to "truth in Z") is semi-decidable and fully formalisable in HOL. On the more detailed suggestions, the only functions over types, as such, are type constructors, which cannot take numeric parameters. However the effect of functions over types, insofar as they depend only on the cardinality of the type, can be realised. A predicate of type: num -> * -> BOOL could be defined which would ignore the value of the second parameter but would indicate whether the size of its type is or is not greater than the nth power of Nat. However, the principled objections mentioned above suggest that this would not suffice to secure the desired embedding. Roger Jones </body> </html>