Reading that ZFC has countable models spooked me. How can uncountable sets exist and an axiomatization of set-theory have a countable model? For a fraction of a second it made me doubt mathematics was real. For a few seconds after that I was thinking of giving up on understanding maths, or at least logic. Then I realized that there had to be a trick about it that made everything make sense again.
There is, yeah. If we look at a countable model of ZFC, and examine one of the sets that the model claims to be uncountable, we’ll find that the set is actually countable. We’ll also find, however, that the model doesn’t contain any surjective function from the natural numbers to that set. So the set will be “uncountable in the model”, in a sense.
A fact that I find spooky is that there is no computable set of first-order axioms that uniquely defines the natural numbers. You can only define them uniquely in second-order logic. But second-order logic doesn’t seem to have a well-defined semantics. (If I’m not mistaken, the continuum hypothesis can be written in SOL without having to use ZFC or anything like that. But the continuum hypothesis doesn’t have a well-defined answer.) These two facts, together, suggest that the natural numbers aren’t actually well-defined at all. And this would mean that provability in a formal system isn’t well-defined, either.
Reading that ZFC has countable models spooked me. How can uncountable sets exist and an axiomatization of set-theory have a countable model? For a fraction of a second it made me doubt mathematics was real. For a few seconds after that I was thinking of giving up on understanding maths, or at least logic. Then I realized that there had to be a trick about it that made everything make sense again.
There is, yeah. If we look at a countable model of ZFC, and examine one of the sets that the model claims to be uncountable, we’ll find that the set is actually countable. We’ll also find, however, that the model doesn’t contain any surjective function from the natural numbers to that set. So the set will be “uncountable in the model”, in a sense.
A fact that I find spooky is that there is no computable set of first-order axioms that uniquely defines the natural numbers. You can only define them uniquely in second-order logic. But second-order logic doesn’t seem to have a well-defined semantics. (If I’m not mistaken, the continuum hypothesis can be written in SOL without having to use ZFC or anything like that. But the continuum hypothesis doesn’t have a well-defined answer.) These two facts, together, suggest that the natural numbers aren’t actually well-defined at all. And this would mean that provability in a formal system isn’t well-defined, either.