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

[roux cody]

Hi Mario,

 You've probably found Forster's "Weak systems of Set Theory Related to HOL"

https://www.dpmms.cam.ac.uk/~tf/maltapaper.ps

Which clarifies things a bit: HOL is *exactly* as strong as "Mac Lane set
theory", which is Zermelo set theory with only *bounded* comprehension (no
quantifiers over all sets)
and so is quite weaker than Zermelo set theory *per se*.

A nice article by Alexandre Miquel describes a variant of HOL (which allows
additional quantifications) that is *exactly* as powerful as Z: they are
equiconsistent (in PA).

"lambda Z: Zermelo's Set Theory as a PTS with 4 Sorts"

http://dl.acm.org/citation.cfm?id=2150524

This rather nicely settles the question of finding a type theory as
powerful as Z set theory. I think ZF is considerably more difficult, and as
far as I know the question is still open.

Best,

Cody


On Tue, Jan 6, 2015 at 4:48 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/20150107/e15c91a1/attachment-0001.html>