[opentheory-users] Embedding Z (or other ZFC fragments) in HOL

[Thomas Forster]

Roger,

Thanks for copying me in and reminding me. It's probably time i had another 
look at this question, but it does sound as if HOL should be equivalent to 
Mac/KF. Since i wrote that article i have been exposed to the notion of 
*synonymy* and a good question might be whether or not HOL is synonymous 
with Mac and KF...


On Jan 7 2015, Roger Bishop Jones wrote:

>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
>    https://www.dpmms.cam.ac.uk/~tf/
>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
>
>
>
>
>
>
>