@Multicore I accidentally deleted your contribution by submitting an edit I started writing before you published yours. I'm letting you add it back so it remains attributed to you. Also, if you can do some relevance voting that would be helpful.
This is one of two ways I know of proving Löb's theorem, and I find them both illuminating. (The other is to derive it from Gödel's Second Incompleteness Theorem.)
Something I learnt from Mietek Bak is that Löb's Theorem is kind of more subtle than this. In provability theory, it's fine to have a "box" operator that we informally read as "is provable"; but what Löb's theorem tells us that we can't simply interpret it literally as "is provable" without difficulties. One should define the "provability" predicate formally, to avoid getting confused (or one should specify that it is simply a formal symbol to which we have not assigned any semantic meaning, although that is somewhat against the point of the angle taken by the parent article); for example, the provability predicate could be defined by a certain first-order formula which unpacks a Gödel number, checks it's encoding a proof and verifies each step of the encoded proof.
@Multicore I accidentally deleted your contribution by submitting an edit I started writing before you published yours. I'm letting you add it back so it remains attributed to you. Also, if you can do some relevance voting that would be helpful.
This is one of two ways I know of proving Löb's theorem, and I find them both illuminating. (The other is to derive it from Gödel's Second Incompleteness Theorem.)
:, not '
Something I learnt from Mietek Bak is that Löb's Theorem is kind of more subtle than this. In provability theory, it's fine to have a "box" operator that we informally read as "is provable"; but what Löb's theorem tells us that we can't simply interpret it literally as "is provable" without difficulties. One should define the "provability" predicate formally, to avoid getting confused (or one should specify that it is simply a formal symbol to which we have not assigned any semantic meaning, although that is somewhat against the point of the angle taken by the parent article); for example, the provability predicate could be defined by a certain first-order formula which unpacks a Gödel number, checks it's encoding a proof and verifies each step of the encoded proof.
Yeah, that is the formal definition of the standard provability predicate. I'll add the page explaining that soon enough.