News for hackers. Stuff that matters.
Re:BusyBeaver(6) Is Quite Large by czbot on Saturday June 28, 2025 @04:27PM (#44407908)
ZFC allows models of second order PA and proves that those models are all isomorphic. Within each model of ZFC there is no such thing as a nonstandard model of second order PA. One can only think it is nonstandard by looking from outside the model, no? What theorem of second order PA is ZFC unable to prove?

This is similar to how there are countable models of ZFC but those models think of themselves as uncountable. They are countable externally and not internally.

Re:BusyBeaver(6) Is Quite Large by cevi on Saturday June 28, 2025 @10:43PM (#44409947)
The consistency of ZFC is (presumably) a theorem of second order PA, and ZFC is unable to prove it (unless ZFC is inconsistent).
Re:BusyBeaver(6) Is Quite Large by czbot on Sunday June 29, 2025 @10:37AM (#44413514)
Indeed yes. But in a sense within ZFC one can say what N is given the categorical nature of second order PA. Each model of ZFC will have, up to isomorphism, one model of N.