[FOM] MK |- CON(ZF) ?

[Chris Scambler]

Thanks for this; I wonder if you could hint at the way in which Pi_1^1
comprehension is used here? I had thought one could make do with Sigma_1^1
separation for sets (one needs to prove the existence of the set of natural
numbers n for which there is a satisfaction class for each Sigma_n formula,
which features a second-order existential quantifier), but perhaps I'm
wrong or missing something.

Thanks!

C
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160516/7651cd23/attachment.html>