Timeline for Which kind of foundation are mathematicians using when proving metatheorems?
Current License: CC BY-SA 3.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 31, 2017 at 19:36 | history | edited | Nik Weaver | CC BY-SA 3.0 |
added 98 characters in body
|
| Jan 31, 2017 at 19:35 | comment | added | Nik Weaver | @AndreasBlass: you're right, I was sloppy. I'll fix it. | |
| Jan 31, 2017 at 19:25 | comment | added | Andreas Blass | If one can prove Con(SEAR) in ZFC${}^+$, then one cannot prove Con(SEAR)$\implies$Con(ZFC) in Peano arithmetic, because, by combining the two along with Con(ZFC)$\implies$Con(ZFC${}^+$), we'd get that ZFC${}^+$ proves its own consistency. | |
| Jan 31, 2017 at 18:23 | comment | added | Nik Weaver | @JohannesHahn: you can't prove in ZFC${}^+$ that ZFC has any model, transitive or not, assuming ZFC is consistent. You can only prove that any finite fragment of ZFC has a model (which can already be done in ZFC). (This is the idea of why ZFC and ZFC${}^+$ are equiconsistent.) | |
| Jan 31, 2017 at 18:12 | comment | added | Johannes Hahn | Wait, what? Isn't the existence of a transitive model of ZFC strictly stronger than the existence of just any model? | |
| Jan 31, 2017 at 15:58 | history | answered | Nik Weaver | CC BY-SA 3.0 |