[dwohnitmok]

> The linked article is about how the theorems destroyed Whitehead et al's aspirations to find One Algebra To Rule Them All.

Sort of. Whitehead's contributions to universal algebra are still relevant and universal algebra is still a thriving field of study for mathematical logic. Although perhaps you mean "algebra" in a more informal sense?

Again, the conclusion of the article is a bit strong.

> Gödel’s proof killed the search for a consistent, complete mathematical system.

The consistency half doesn't make sense. (EDIT: I get it now, see the last sentence of this paragraph) There was never a search for a consistent mathematical system in the sense that Godel destroyed because again a system that can prove its own consistency has no positive value in evaluating the consistency of that system (Godel's big contribution here is contributing a strong negative result, if it could prove its own consistency you're pretty screwed). EDIT: On reflection I see that the sentence probably means to tie consistency to completeness rather than as a stand-alone quality. That makes more sense.

As for mathematicians, their reactions to Godel's incompleteness theorems overall are probably similar to "Who cares about your incompleteness theorems?" (there's a reason Russell and Whitehead are known primarily for being philosophers first and mathematicians second and why often times there is distinction between logicians like Godel and other mathematicians). Most mathematicians don't think about the foundations of mathematics because it is (perhaps surprisingly) largely irrelevant to the day-to-day work of mathematicians. Indeed the vast majority of mathematics is very resilient to changes in its underlying foundations.

To interpret Godel's incompleteness theorems requires a healthy dose of at least mathematical logic that can start veering quite close to mathematical philosophy.

An example from the article:

> However, although G is undecidable, it’s clearly true. G says, “The formula with Gödel number sub(n, n, 17) cannot be proved,” and that’s exactly what we’ve found to be the case!

Well no, that's not true in certain senses. Indeed in a larger axiomatic system subsuming the current system that corresponds to G, it is completely consistent to state that G is provable and that its statement is provable (see my example of S'), i.e. there are Godel numbers that correspond to both a proof of G and to a proof of its content. To interpret that statement that way requires certain philosophical commitments to the correspondence between a Godel number and truth, which not everyone would accept (do you accept the truth of the new axiom introduced by S'? Why then do you accept the truth of the statement "S is consistent?" and vice versa).

"In striving for a complete mathematical system, you can never catch your own tail." This on the other hand I think is a very good informal description of what's on with Godel's incompleteness theorems. Focus on the incompleteness not on truth.

That's why I'm not a fan of using the word "truth" when talking about Godel's incompleteness theorems. I am in fact deeply sympathetic to your desire to separate philosophy from Godel's incompleteness theorems.

I prefer to clearly delineate between its logical properties in mathematical logic and its philosophical implications and using the word "truth" by necessity muddles the two.

FINAL EDIT: I am being perhaps a bit too harsh on the article. I think it does a fine job of describing the arithmetization of the incompleteness theorems. But if someone else reading this also decides to create an informal guide to Godel's incompleteness theorems, please please please don't use the word "truth" and "true" or at least separate it out into its own section on philosophy.

[pdonis]

> that's not true in certain senses

I think it's not true in a very clear sense: you can construct semantic models of the axioms of arithmetic in which it is false. In other words, you can construct semantic models of the axioms of arithmetic (more precisely, of the axioms of arithmetic using first-order logic, which is what the article is about) in which there is a "number" that is the Godel number of a proof of the Godel sentence G! Godel's Theorem just ensures that in any such model, the "number" that is the Godel number of such a proof will not be a "standard" natural number, i.e., one that you can obtain from zero via the application of the successor operation.

So another way of viewing this whole issue of "truth" is that it is always relative to some semantic model. If your chosen semantic model of the axioms of arithmetic is the "standard" natural numbers, and only those numbers, then the Godel sentence G for that system will be true--there will indeed be no number in your model that is the Godel number of a proof of G. But if you pick instead a non-standard model that includes "numbers" other than the standard natural numbers, but still satisfies the axioms, then the Godel sentence G can be false in that model, since there can exist a "number" (just not a standard one) in that model that is the Godel number of a proof of G.

[dwohnitmok]

What you are saying is true (as you allude to with first-order logic) in any context in which Godel's completeness (not incompleteness) theorem holds. Not all logics have versions of Godel's completeness theorem (e.g. second order logic with full semantics). You can argue that philosophically in systems where Godel's completeness theorem fails that the article's statement is valid. But yes that's why it's only true in "certain senses."

More generally the philosophical question of truth revolves around whether there is a single, true set of standard natural numbers that corresponds to reality, and therefore all nonstandard natural numbers are "artificial" in some sense, or whether even standard natural numbers exist only in a relative sense.

[krick]

You seem like somebody who I could ask some (2) questions on the topic.

1. First of, I'm still not sure what to make of Gödel's theorems philosophically. In the "pop-culture", so to speak, there seems to be a notion that Gödel's theorems are, in essence, some grand, weighty statement about fundamental "inaccessibility of truth". That since Peano's arithmetic exemplifies very simple (compared to our general needs) mathematical system, no matter how we further develop math, one day there will be a useful, meaningful statement which cannot be proved or disproved.

What's perhaps even worse, some people, even some with names I feel uncomfortable to argue against (Penrose, for example, seems to be of this opinion) try to use it as a transition to the idea that "human mind is more than a computer", which I always implicitly assumed to be just a manifestation of anthropocentric hubris. The key to their reasoning is the observation, that some expressions unprovable within some formal system are "obviously true" (and they often kinda are, and they are provable within a higher-order formal system). So, the story goes, since the Turing machine couldn't see it (because of Gödel's), but we see it, we are more than a Turing machine.

And since that informal version of Gödel's findings was familiar to me long before I was acquainted with a formal version of it, I'm kinda used to the idea that "it must be right".

However, when I'm looking at the formal explanation of Gödel's theorems, or even perhaps more interesting "applied" findings, based on them (like Goodstein's theorem), they all seem to be surprisingly "boring" and non-consequential clever tricks based on self-referencing. I mean, it's sure a very interesting finding about formal systems as such, but if we take a step back into the realms of common sense: isn't it rather quite intuitive, that a system cannot be proven to be consistent by the means of the same system? So it must be of no surprise that any formal system powerful enough to be able to express statements about consistency of itself must be "incomplete".

So, my question is, am I missing something? Is there any truth to that pop-cultural image of Gödel's theorems? Because to me it seems like there actually isn't, just more of an "urban myth".

2. Continuum hypothesis. As I understand it, it is a matter of axiom, if 2^Aleph₀ ?= Aleph₁ and |R| could be as well Aleph₅ or whatever. Of course, we have most natural axiomatic system (with axiom of determinacy) where the former is true. But are there, like it was with Euclid's fifth postulate, any alternative, but still "interesting" constructs? Is there any use whatsoever in the assertion that continuum hypothesis is false?

[dwohnitmok]

I'll give brief statements with lots of hand-waving since I'm low on time. These are long questions.

1. In short, this is a deeply philosophical question. My personal inclination follows yours that the incompleteness theorems are overhyped. I don't buy Penrose's argument. Like most other formal limiting results philosophically I view those results as representing fundamental limits of both human and machine reasoning. While a single unproveable but "obviously true" result generally point to an inadequacy of the formal system, if every formal system suffers from some inadequacy that is indicative of a limitation in the fundamental human faculties of comprehension rather than a limitation of formal systems per se (the assumption e.g. that our formal systems must use finitistic methods is one born of human limitations and, depending on one's thoughts about the universe, potentially fundamental physical ones).

There are philosophically defensible positions that try to claim the incompleteness theorems have implications for truth in the real world, but I go back and forth on whether I believe them and more to the point they are far more subtle than the usual pop culture presentations of Godel's incompleteness theorems.

2. The mathematical Platonists I've come across believe that the continuum hypothesis is in fact false. (As an aside it's interesting that you find the axiom of determinacy natural as it contradicts the axiom of choice.) This mainly hinges on your opinion of the reality of large cardinals (which perhaps count as your "interesting" constructs), which many Platonists for a variety of reasons believe to be real.