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

[Mario Carneiro]

Hello all,

I'm trying to locate any research done on what kinds of subsystems of ZFC
can be embedded into higher order logic. My initial approach on the subject
leads me to believe that HOL can embed any proof in Z, using the following
method:

HOL contains types of cardinality om (omega), ~P om, ~P ~P om, etc for any
finite number of ~P's (the powerset operation). Since any particular proof
in Z will use the theorems "om e. V" (omega exists) and "x e. V -> ~P x e.
V" (a powerset exists) finitely many times, you could define a function on
types (does such a thing exist?) saying that a type A is "n-large" meaning
there is an injection from ~P ~P ... ~P om to A (where there are n ~P
symbols), and then a proof in Z would get V mapped to an arbitrary type A,
and if there are n ~P's used in the proof you would preface the entire
proof with "A is n-large". When you are done and ready to map the model
back to the regular HOL notions, you replace A with ind->bool->...->bool (n
times), and then prove that this type is n-large to discharge the extra
assumption.

Does anyone know of any papers or work done in the direction of embedding
fragments of ZFC in HOL like this?

Mario Carneiro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150106/f1623f16/attachment.html>