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

[Josef Urban]

Hi Mario,

I do not know the Z fragment, but the main issues in ZFC vs HOL seem to be:
(1) the HOL type discipline prevents you to mix sets of different types,
and (2) the HOL axioms are too weak to allow transfinite constructions.

Off the top of my head, I am aware of the following:

- the HOLZF work in Isabelle by Obua, just axiomatizing ZF(C?) as a type
(practically adding an inaccessible cardinal axiom instead of just omega)

- a bridge between Isabelle/ZF and Isabelle/Hol by Krauss (I do not know
the details)

- Kuncar's MS work on importing the Mizar soft typing mechanisms into HOL
(Light), again embedding the whole ZFC there as a separate type

- Mike Gordon's older paper discussing various options how to link ZF and
HOL

Josef
 On Jan 8, 2015 1:32 AM, "Mario Carneiro" <di.gama at gmail.com> wrote:

> 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
>
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20150108/9cdefb13/attachment-0001.html>