alt Hacker NewsI think this is selling Gödel a little bit short. He proved for the first time that in any system of mathematics with enough complexity to be interesting, there are statements that cannot be proven true or false. The Gödel sentence might seem like a trivial example, but other examples of such things have been discovered since, such as the continuum hypothesis which the article mentions.
Replies
> enough complexity to be interesting
That's the loophole. There is mathematics without infinity.[1] Until recently, it was considered somewhat fringe. But there's been enough development that it's now clear you can do mathematics without infinity. In that view, infinities are a labor-saving device to get rid of special cases. They're not essential. Mathematicians used to hate special cases, but now that the active ones all grew up with computers, they're not so scared of IF statements.
You can have "arbitrarily large" but not "infinite". Boyer-Moore theory is like that. It starts out like Peano arithmetic. There is (ZERO) and (ADD1 (ZERO)) and (EQUALP A B) and (LESSP A B) as predicates. That's the axiomatic basis. Numbers are (ADD1 (ADD1 (ADD1 (ZERO)))), etc.
You can have recursive functions, but they must terminate. They must have a value which, for each recursion, is LESSP than the previous iteration. That's how you prove termination.
You can do most of mathematics that way. But not infinitesimals. You never can get to
1 + 1/2 + 1/4 + 1/8 ... = 2
[1] https://engtechnica.com/rethinking-mathematics-without-infin...
> n any system of mathematics with enough complexity to be interesting, there are statements that cannot be proven true or false.
Note that the article itself is not as careful as you are here about correctly stating what Godel's Incompleteness Theorem actually says. The article states it this way: "any set of rules powerful enough to handle basic arithmetic will contain true statements it cannot prove". But that's wrong, because, when you take into account Godel's Completeness Theorem, you realize that, for any formal system complex enough for the proof of Godel's Incompleteness Theorem to go through, there must be a semantic model of that system in which the Godel sentence for that system is false! The article's misstatement is unfortunately very common, but it's still a misstatement.
The Gödel sentence (which is not otherwise of any interest) is true but unprovable within that axiomatic system. The Continuum hypothesis (which is of great interest) is true or false only by stipulation.
The fact is that neither Gödel's theorems nor the Halting Problem have any actual real world consequences (outside of people talking about them). People say "oh, we can't write a verifier because of the Halting Problem", but that's simply not true since all of our programs are actually FSMs with physically limited data, and the HP is solvable for that subset of TMs. The real limitations are time and space, so this is an engineering problem -- and people who aren't suckered by Halting Problem Hysteria find engineering solutions that work on real programs, bailing if memory or time thresholds are exceeded.
The article is massively overstating the implications of Godel to the AI industry, so to be clear - are you defending the article, or are we bikeshedding about my phrasing? Because my "not that profound" should be interpreted as relative to the article.