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

[Roger Bishop Jones]

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






-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150107/77ca5169/attachment.html>