I often read paraphrases of one or other of Gödel’s theorems that talk about true, unprovable statements. I’ve said before that I’m a formalist of sorts. Talk of undecidable statements in a system being true gives me headaches. And I’m an analyst so I work in ZFC. If I say “statement X is true” I’m telling you that there exists a proof of statement X in ZFC. If you ask me if I think the continuum hypothesis is true, I’ll explain to you that it’s known to be undecidable. If you tell me you know it’s undecidable but still want to know if I think it’s true, I’ll look at you as if you asked me what colour integrity is.
If it was clear that the question “Is X true?” didn’t mean “Can X be proven in ZFC?”, say the question was “Is the Axiom of Choice true?”, I guess I’d them take an explicitly formalist stance: “I don’t think that either AC or its negation is truer than the other; the term “true” doesn’t really mean anything in this context”. We analysts pretty much always work using the axiom of choice, but for reasons that don’t have anything to do with delcaring it to be “really, really true”. We use choice because it’s better for doing the maths in. Results would need expressing in tiresomely fussy ways if we couldn’t reach for Zorn’s lemma or the Hahn-Banach theorem.
So, “true” is a word I might use to talk about maths but “true” as I would ever use it isn’t itself maths; the meaning is a bit slippery as you would expect for a word in a natural language. Also any uses I would give it wouldn’t be allowed to slip outside a particular system. I don’t think this is a particularly unusually position for a mathematician to take. All the same writing aimed at non-mathematicians often goes like this by Chad Orzel:
…Kurt Gödel’s famous Incompleteness Theorem, which shows that any formal logical system complex enough to describe arithmetic must allow the formation of statements that are true, but cannot be proved to be true within that system.
Now I’m not saying that this formulation is unsupportable since (some) people who have looked at this very deeply accept it. Roger Penrose always states it like that and I understand Gödel himself saw it that way. Also, at a push, I can sort of see it; the Gödel sentence (which is proved to be undecidable) “says” that a certain number is not the Gödel number of a provable statement in the system. If such a statement existed so would its proof and that proof could be turned into a proof of the negation of the Gödel sentence (which of course we can have). Therefore it is true that the number was not the Gödel number of a provable statement in the system.
OK, but you see those quotation marks around “says”? What if we take a “glibly” formalist view of this; that mathematics is a game played by the formal manipulation of meaningless symbols? Then the formula doesn’t say anything at all; the interpretation may be handy for thinking about it (like thinking of Euclid’s axioms as being about space) but it doesn’t “really say” anything, especially if take them out of the system and look at them on there own. The theorem is (as was cautiously pointed on the In Our Time episode on the subject but is usually ignored in popular treatments) purely syntactic and not necessarily about any semantic interpretation.
Again I’m not saying the version with “true” isn’t true; I’m just saying it is a headache. If it is true, it’s true in a way that’s somewhat complicated. And, note, this is the version we see in things for a general audience.
Help me out here; is it really that laypeople can understand this with no trouble, but it makes my mathematician’s head explode? Or is it that the popularizations are actually close to incomprehensible but people just don’t notice because they are typically happy with intuition that statements are (“really”) either true or false?