Conway's Game of Life is a kind of reality summarized into axioms and rules, and most likely our universe/multiverse is on track to being similarly summarized. The halting issue doesn't get in the way of that achievement...
Once you have the intuition for why the Halting Problem (i.e. fortune teller paradox) is obvious, then Godel's proof is just an XSS attack on axiom systems whose designers think they're only "about numbers", like how CSS is designed to be about styling but it's also Turing-complete and vulnerable to XSS.
Russel and Whitehead were trying to simultaneously (1) invent a system capable of proving highly insightful claims about the infinite space of numbers, like "there doesn't exist a number between 1 and infinity with property P" but (2) not a system that can encode a Turing-equivalent agent that creates paradoxes if it tries to predict its own future.
Godel was just the first to point out that condition (2) was already met just by supporting Peano Arithmetic, the same way a modern computer science undergrad can point out that CSS is Turing-complete or your regex-based HTML validator is vulnerable to XSS attacks.
[1] https://stackoverflow.com/questions/2497146/is-css-turing-co...
[1] https://stackoverflow.com/questions/3607894/cross-site-scrip...
The predicate Halt<aType>[anExpression] is true if and only
if anExpression of type aType halts.
The predicate Halt is inferentially undecidable, that is, it
is not the case that for every expression anExpression of type aType that
|- Halt<aType>[anExpression] or |- ~Halt<aType>[anExpression].
Inferential undecidability does not mean that mathematics
is wrong.
Of course, it is possible to have incorrect
mathematical proofs, such as the incorrect proof in
[Gödel 1931] for the inferential undecidability of Russell's
Principia Mathematica. (There is a correct proof here:
Of course proofs can be still correct, it's just that we cannot cope with infinites very well without talking about computational limits.
My argument was hyperbolic, I regret, but it was less about what's incorrect and more about what's incomplete. The aspirations of early mathematicians was to discover a platonic ideal. Instead of that we only got useful tools that are always* up for re-interpretation depending on context.
An example of this is that Euclid's fifth postulate, which be consistent with many other interpretations of geometry too, not just the single one originally intended. It turned into a tool of formal scaffolding instead of an omnipotent "truth". Going from absolute to relative in power.
*In cases where they involve infinites. Including simple expressions like "take N to be an integer"