> 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 min

> 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.pdf https://categorified.net/FreshmanSeminar2014/Lobs-Theorem.pd...