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.
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.