Hacker News Reader

Comment by Liron | Hacker News Reader

People act like Godel’s Incompleteness Theorem is all about how formal systems are limited in their level of “insight about truth”. But actually it’s just the same observation as the Halting Problem: you have a system that tries to reason about the behavior of other systems (like Turing Machines or axiomatic set theory), but it can’t possibly always introspect about its own behavior because you can also configure it to behave differently based on its own conclusion about its behavior.

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.

View on HN

While this is true, it is surprising that is it impossible to engineer a system to be complete and consistent about arithmetic, as opposed to systems which are not engineered well, like your 2nd paragraph.

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.

Russel and Whitehead's system is well-engineered; that's why it doesn't prove a contradiction (presumably) while your badly engineered system does. The issue is that R&W made their system powerful enough that it's also incomplete, due to the fact that their system contains smartass statements like G that are hell-bent on creating paradoxes if given the chance.

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.

Russell's Principia Mathematica (PM) is indeed better

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.

Because of the halting issue you cannot summarise reality into a set of axioms and rules. Which is the original purpose of mathematics. Therefore you cannot say mathematics is right or true without adding at the end: "this actually could all be wrong".

at the end: maybe not even wrong

> Because of the halting issue you cannot summarise reality into a set of axioms and rules

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.

CSS is not turing-complete - it is as turing-complete as a simple TXT file. Deciding whether some sequence of bytes resembles a CSS file is very possible. Deciding whether a stylesheet can be successfully applied to a website is also decidable. Of course, it is undecidable whether a certain pattern emerges if a stylesheet is applied to an infinitely large HTML file. But then, it is also undecidable whether some TXT file appears in an infinitely large HTML file.

It's Turing complete if you let a human feed a bunch of clicks to proceed along the computation steps. [1] It also allows embedded JS (in some browsers), which is Turing complete. My point is that languages really quickly surpass the Turing complete barrier if you let them do fancy things. Godel realized that proving interesting statements about unbounded natural numbers is quite a fancy thing.

[1] https://stackoverflow.com/questions/2497146/is-css-turing-co...

This is not vital to the point you’re making but XSS has nothing to do with CSS.

In this case the XSS vector is the fact that CSS allows running JavaScript in some browsers [1], but still, a lot of systems that are supposed to be weak and domain-specific are discovered to be Turing-complete, e.g. Conway's Game of Life.

[1] https://stackoverflow.com/questions/3607894/cross-site-scrip...

Dear Darlthus,

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:

https://papers.ssrn.com/abstract=3603021)

Thank you for the paper.

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"

Hi Liron,

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.

See https://papers.ssrn.com/abstract=3603021

   However, the [Gödel 1931] proof is incorrect for reasons
   mentioned elsewhere in this discussion.

Reply on news.ycombinator.com