Surprises in Logic (2016)

Another weird one related to Gödel’s theorems is Löb’s theorem: given a sound formal system F and a sentence s, if F proves that “if s is provable in F, then s,” then F also proves s. That is:

F ⊢ (Prov_F(“s”) → s) → s

Which is strange because you might think that proving “if s is provable, then s” would be possible regardless of whether s is actually provable. But Löb’s theorem shows that such self-referential statements can only be proven when s itself is already provable.

> F ⊢ (Prov_F(“s”) → s) → s

This is called "Löb’s hypothesis" and it's an incredible piece of logical machinery[1]. If you truly understand it, it's pretty mind-blowing that it's actually a logically sound statement. It's one of my favorite ways to prove Gödel's Second Theorem of Incompleteness.

[1] https://categorified.net/FreshmanSeminar2014/Lobs-Theorem.pd...

"If this sentence is true, then Germany borders China."

not yet