What if I ask you to predict whether you’re going to go left or right, but I also tell you that I’m going to force you to go the opposite direction as what you predict? Then the set of things you can accurately predict is Incomplete. But that’s not a profound limitation of human consciousness, it’s just the familiar paradox of any fortune teller or time travel scenarios.
If I take "1 is even", "1 is odd" and "no number can be even and odd" as my axioms, then there is obviously a problem, but of my own doing.
Before Godel's time, people just didn't have enough experience with computers to realize that you have to deal with code injection attacks every time you try to build a powerful platform of any kind. In this case, Godel Numbering is the hack that allows code injection into a formal system that's supposed to just be highly insightful about properties of the infinite world of natural numbers.
engineered than its predecessor by Frege because it has orders
on propositions. Because of orders on proportions, PM does
not allow the [Gödel 1931] proposition I'mUnprovable.
Furthermore, adding the proposition I'mUnprovable would
make PM inconsistent.
The Gödel number of a proposition in PM is itself
"incomplete" because it *doesn't* include the order of the
proposition. Allowing its Gödel number to represent a
proposition is indeed a kind of "code injection" attack,
which if allowed would make PM inconsistent.
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.
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
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"
Your intuition is pretty good.
A correct proof of inferential incompleteness of Russell's
Principia Mathematica can be constructed using the
computational undecidability of the halting problem.
However, the [Gödel 1931] proof is incorrect for reasons
mentioned elsewhere in this discussion.