I think Jessica is right on this point. Within a system like ZFC, you can’t define the system’s own definability predicate, so the sentence “there are numbers undefinable in ZFC” can’t even be said, let alone proved. (Which is just as well, since ZFC has a countable model, and even a model whose every member is definable.) The same applies to the system of everything you believe about math, as long as it’s consistent and at least as strong as ZFC.
I think Jessica is right on this point. Within a system like ZFC, you can’t define the system’s own definability predicate, so the sentence “there are numbers undefinable in ZFC” can’t even be said, let alone proved. (Which is just as well, since ZFC has a countable model, and even a model whose every member is definable.) The same applies to the system of everything you believe about math, as long as it’s consistent and at least as strong as ZFC.