My beliefs about the integers are a little fuzzy. I believe the things that ZFC can prove about the integers, but there seems to be more than that. In particular, I intuitively believe that "my beliefs about the integers are consistent, because the integers exist". That's an uncomfortable situation to be in, because we know that a consistent theory can't assert its own consistency.
Should I conclude that my beliefs about the integers can't be covered by any single formal theory? That's a tempting line of thought, but it reminds me of all these people claiming that the human mind is uncomputable, or that humans will always be smarter than machines. It feels like being on the wrong side of history.
It's also dangerous to believe that "the integers exist" due to my having clear intuitions about them, because humans sometimes make mistakes. Before Russell's paradox, someone could be forgiven for thinking that the objects of naive set theory "exist" because they have clear intuitions about sets, but they would be wrong nonetheless.
Let's explore the other direction instead. What if there was some way to extrapolate my fuzzy beliefs about the integers? In full generality, the outcome of such a process should be a Turing machine that prints sentences about integers which I believe in. Such a machine would encode some effectively generated theory about the integers, which we know cannot assert its own consistency and be consistent at the same time.
So it seems that in the process of extracting my "consistent extrapolated beliefs", something has to give. At some point, my belief in my own consistency has to go, if I want the final result to be consistent.
But if I already know that much about the outcome, it might make sense for me to change my beliefs now, and end up with something like this: "All my beliefs about the integers follow from some specific formal theory that I don't know yet. In particular, I don't believe that my beliefs about the integers are consistent."
I'm not sure if there are gaps in the above reasoning, and I don't know if using probabilistic reflection changes the conclusions any. What do you think?
I think you're imagining an exit that isn't there. For example, ZFC can formalize Gentzen's proof of consistency of PA, and supports quite a bit of transfinite induction. Yet it still has to obey Gödel's theorem, like any other recursively axiomatizable theory.
(Also, all sets of axioms are countable, because they are subsets of the set of all finite strings, which is countable. I assume you meant to say something else, but I can't guess what.)
The amazing thing about Gödel's theorem is how general it is. I mentioned that in the post. Any Turing machine that prints theorems (regardless of the internal mechanism) must obey Gödelian limitations, as must any Turing machine that receives proofs and checks them for correctness by any method. The only way to escape these limits is by hypercomputation, but I wouldn't hold my breath.
I don't doubt that just about anything can be formalized in ZFC or some extension of it. I am aware that a Turing machine can print any recursively axiomatizable theory.
The set of all finite strings is clearly order-able. Anything constructed from subsets of this set is countable in that it has cardinality aleph_1 or less (even if it contains the set).
I read this book on something called language theory (I think it's now called "formal language theory")... (read more)