Assume the Hilbert-Bernays-Löb derivability conditions and the diagonal lemma. If proves for every sentence , then . Take the single instance and discharge the assumption: . This propositionally implies , and Löb's theorem gives . A diagonal proof is also possible using the Gödel sentence of the extension and formalized proof transfer, without appealing to Löb's theorem.
Articles by others on the same topic
There are currently no matching articles.