Brought to you by into the continuum:

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’tbe 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:⊢⊬⊬XSo 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).

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