Brought to you by

To paraphrase Boolos paraphrasing Gödel paraphrasing himself:

It is true that 2 plus 2 is 4. I hope you can at least believe that much. Of course, it can be proved ⊢ that 2 plus 2 is 4. It can also be proved that it can be proved ⊢⊢ that 2 plus 2 is 4.

Moreover, it can be proved that it can be proved that it can be proved ⊢⊢⊢ that 2 plus 2 is 4. We could continue in this seemingly trivial manner, but what we are hoping for is that 2 plus 2 is not 5. Fortunately, it can be proved ⊢ that 2 plus 2 is not 5, and that too can be proved ⊢⊢.

Now just to be on the safe side what we really should ask is if it can be proved that it can’t be proved ⊢⊬ that 2 plus 2 is 5…. It can’t! ⊬ ⊢⊬ In fact, no claim of the form “claim X can’t be proved” can be proved.`∀X:(⊢⊬X)→⊥ or `∀X:⊬X

So thanks to Gödel … it can be proved that if it can be proved that it can’t be proved that 2 plus 2 is 5, then it can be proved that 2 plus 2 is 5. `⊢(⊢⊬X→⊢X)` [Which is a contradiction.] I would rather take an incomplete theory over [an unquestionably wrong, self-]inconsistent one any day. Wouldn’t you?

… pretty tanpura drones in the pitches of `C#` and `A`, respectively (which I suggest listening to with eyes closed and nice headphones).

• `C#`
• `A`

If on reading that you thought: “the ⊢⊬⊢⊢ symbols…could you do math with those operators?” then here’s some more at the SEP.

Gödel’s incompleteness theorem in small words