I 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.
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.
Ah that "with me or against me" dichotomy again.
> 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
in that kind of constructive mathematics. That requires an infinite recursion, which is not allowed.[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.