We also have another theorem of PA asserting that this theorem is provable:
Is this theorem a premise, or derived from another theorem? I disagree with the inclusion of this theorem.
I’m not disagreeing about what your argument would prove, if the premises were all correct. I agree that it does, indeed, prove an equivalence between the Payorian FairBot and the Löbian FairBot, modulo certain other assumptions. But those other assumptions are non-trivial, and the two FairBots are in fact different, precisely when those other assumptions break down.
Okay, that I can answer. It’s derived from the previous theorem, as follows.
The following means that is a thereom of PA, which by definition means there’s a proof of it:
Let be the sentence in PA that asserts is provable, that is, that asserts there exists a number which is a Gödel number of a proof of the sentence with Gödel number .
Take the proof of and convert it to its Gödel number. That satisfies the existence statement , so we have a constructive proof of it. So we have:
And I’m using the box to represent PA’s provability predicate, so that’s:
Does that make sense?
I should definitely edit the post. I at least need to clearly claim it follows from the previous theorem.
I wonder if there’s a short way to indicate this whole line of reasoning. I guess if I just want to point to the principle, it’s the first of the Löb provability conditions, but I’d rather indicate why it’s true.
No problem, I edited and it looks a lot better now.
With that cleared up I do want to get back to the root of this thread, because it’s genuinely weird that the FairBot pseudocode in the paper has a branch where it says “if there’s no proof, return D”. But it’s getting late here so I’ll have to do that another day.
Is this theorem a premise, or derived from another theorem? I disagree with the inclusion of this theorem.
I’m not disagreeing about what your argument would prove, if the premises were all correct. I agree that it does, indeed, prove an equivalence between the Payorian FairBot and the Löbian FairBot, modulo certain other assumptions. But those other assumptions are non-trivial, and the two FairBots are in fact different, precisely when those other assumptions break down.
Okay, that I can answer. It’s derived from the previous theorem, as follows.
The following means that
Let
Take the proof of
And I’m using the box to represent PA’s provability predicate, so that’s:
Does that make sense?
I should definitely edit the post. I at least need to clearly claim it follows from the previous theorem.
I wonder if there’s a short way to indicate this whole line of reasoning. I guess if I just want to point to the principle, it’s the first of the Löb provability conditions, but I’d rather indicate why it’s true.
Yes, that makes sense! Thanks for explaining.
I think it would have made more sense to me if the GL derivation was written as
No problem, I edited and it looks a lot better now.
With that cleared up I do want to get back to the root of this thread, because it’s genuinely weird that the FairBot pseudocode in the paper has a branch where it says “if there’s no proof, return D”. But it’s getting late here so I’ll have to do that another day.