this is my favorite of all the symbolic representations of Gödel's Incompleteness Theorem I've seen so far
this is how it appears in the first chapter of Boolos's book The Logic of Provability, and the logic being used here is called "GL", or just "provability logic"
here we see the "¬" symbol playing its usual role as logical negation ("not")
the falsum, "⊥", is also a standard logical symbol, and stands for falsity (the proposition which is never true; a contradiction)
the arrow "→" of course represents entailment (that which is to the left of "→" entails that which is to the right of it)
less familiar is the (modal) provability operator "□", which declares that its argument (the thing to its right) is provable (in the logic under consideration)
so the stuff to the left of the entailment ("¬□⊥") says that the false proposition is not provable - this is a statement of the consistency of the logic under consideration; it means that we cannot use the rules of our logic to prove a false statement
the stuff to the right of the entailment ("¬□¬□⊥") is just the stuff to the left, with "¬□" ("the following is not provable") stuck in front of it; thus it states that "¬□⊥" (the consistency of our logic) is not provable (within our logic itself); it means that our logic cannot prove its own consistency
and the entire entailment statement thus expresses that any consistent logic founded on GL will be unable to prove its own consistency
we can also rewrite this without negation by defining "¬p" as "p→⊥" ("p is false" is being defined as "p entails a contradiction"), leaving us with
((□⊥)→⊥) → ((□((□⊥)→⊥))→⊥)
"if proving a contradiction entails a contradiction, then proving that proving a contradiction entails a contradiction itself entails a contradiction"
