Is this visual analogy to Gödel's incompleteness theorem accurate?

Question

Today I was trying to explaining the Gödel's theorem to a layman, I've drawn a figure similar to the one below and said that:

• A truth is a consequence of the axioms (with the axioms also being truth).
• The lines between the axioms and the theorems and the lines between theorems and theorems are the employed notions to show the truth of that theorem.
• And that there are theorems that are true (red diamonds) but unreachable by any arrangement of lines from the axioms to the theorems to them. The red lines are meant to show that there is no line that reaches there.

Is this visual analogy accurate? I know that perhaps I'm oversimplifying, but does it captures the big picture or is there something else I should add?

Answer 1

All theorems are provable: that is what the word "theorem" means. The point is that not all truths are provable, that is, not all truths are theorems. IMO your diagram would be more helpful if you replaced the word "theorem" everywhere by "truth" (or something synonymous). Perhaps the box at the top could be labelled "theorems" as well.

Answer 2

Well, first of all I wouldn't call them "theorem" $\infty, ?$, since by definition something's only a theorem if it's provable. :) But this is a very minor criticism.

I like this picture a lot, partly because of the suggestive feel of "if we could make our proofs infinitely long, then we could prove these things!" This can be made precise in a variety of ways, and is true to different degrees depending on how it is made precise, but it is always somewhat true: if we allow "infinitely long proofs" (whatever those may be) then certain at least every true $\Pi^0_1$ statement - such as "PA is consistent" - will be provable.

There are two tiny criticisms I have, though they obviously don't mean it's not cool (like I said above, I like it a lot):

• One, it addresses what it means for something to be not provable; it doesn't explain how one would possibly show that something's not provable, or what such a statement might look like. (Of course, that may well be a job for another picture . . .)

• More subtly, the question "Which kinds of true sentences can be proved if we allow infinitely long proofs?" is incredibly deep and subtle, and a picture like that suggests that the answer is "all of them," which (in most interpretations) it is not.

However, these are very much not big problems. The second one in particular is definitely something I wouldn't worry about until well after one has understood Godel's theorem.

Answer 3

(The best source for this subject is the book "Gödel, Escher, Bach" by Douglas Hofstadter)

First, I agree with the distinction the other answers make about truths and theorems.

Second, I am not sure I like the red dotted lines. To my eye they suggest that there are proofs leading to those statements. If you want to talk about infinitely long proofs, leave them in, otherwise take them out. Gödel's work assumes that proofs are finite, so infinite proofs would be a detour.

Third, I think you might want to add a second half to the figure, with falsehoods and anti-theorems. Anti-theorems being the negation of theorems, statements that are provably false. This could lead to a figure that is too cluttered, though. Your call.

Answer 4

I don't like this:

A truth is a consequence of the axioms (with the axioms also being truth).

You're trying to convey that there are truths which are not consequences of the axioms. So this definition of truth is counterproductive. We could try to come up with another, but I doubt you can define whether (say) the Continuum Hypothesis is true or false without annoying someone. Worse, the CH is precisely the kind of statement we're interested in!

I'm not sure it's a great idea to talk about "truth" here. Instead, focus on the fact that there are some statements which we cannot prove, and whose negations we also cannot prove. Combined with the law of the excluded middle, that helps to suggest the intuition that some of these statements are "true" in some sense, while avoiding a direct definition of truth.