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

[Mario Carneiro]

Thank you to everyone who has provided such great references; this is
exactly what I was looking for.

I think I can see why my proposed translation would fail, since there is a
possibility that unbounded quantifiers in the separation scheme, which
would be translated to bounded quantifiers over a "large enough" set, could
still detect that they are bounded. To take a simple example, the
proposition ( om e. x /\ A. x E. y rank(y) > rank(x) ) would be true in the
intended model V_2om of HOL but false in any type (assuming that types are
mapped to elements of V_2om), no matter how large.

The claim that Z (just so we're on the same page, Z means Zermelo set
theory here) proves Con(HOL) leads me to consider the reverse embedding,
however, by roughly the same method. Define the types 2 = bool and om = ind
as 0-large, and define an n-large set inductively as sets of the form A,
A^B for any n-1-large sets A, B. This is definable in Z, and the set of all
n-large sets for fixed n provably exists in Z. Then any given proof in HOL
will use only n-large sets up to some fixed n, and all these can be proven
to exist. Furthermore, this approach allows one to map HOL + global choice
(which is the way AC is usually formulated in HOL) to ZC, because if you
assume that f is a choice function on all n-large sets for some n large
enough for all the types in the proof, then f can play the role of the @
choice function, and at the end of the proof you can discharge the
assumption by AC.

Mario

On Wed, Jan 7, 2015 at 5:07 PM, roux cody <cody.roux at gmail.com> wrote:

> 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
>>
>>
>
> _______________________________________________
> 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/c0e73e86/attachment.html>