Timeline for Taking a proper class as a model for Set Theory
Current License: CC BY-SA 3.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 16, 2018 at 14:39 | comment | added | Asaf Karagila♦ | The former. The point is that the process of moving from the code of $\varphi$ to the code of the relativization of $\varphi$ to WF (or V) is itself a primitive recursive process. So if you assume in PRA that ZF proves a contradiction, the process of transforming this to a proof of contradiction from ZF-Reg is recursive: just apply the relativization function finitely many times. | |
| Feb 16, 2018 at 14:32 | comment | added | user21820 | Can I ask to clarify something? Did you actually obtain a proof within PRA itself that Con(ZF−F) implies Con(ZF)? Or is it that you prove in ZFC that a proof exists in PRA (as seemingly stated in your answer)? Similarly, what is the weakest well-known system over which we have an actual proof for "Con(Z) implies Con(ZFC)", or at least can write a program to generate the proof? Thanks! | |
| Feb 15, 2018 at 18:25 | comment | added | Asaf Karagila♦ | One might say that Mati was overly pedantic in his teaching methods, by the way. I mean, I would say that, and I know a few other people who would say otherwise. | |
| Feb 15, 2018 at 18:21 | history | answered | Asaf Karagila♦ | CC BY-SA 3.0 |