Right, I know the question isn’t whether the GL derivation is correct.
This is what I want to get on the same page about: do you agree that the GL derivation, with both those premises, establishes that the Löbian FairBot, as defined at the top of my post, must satisfy the condition of a Payorian FairBot, as defined at the top of my post?
This is what I establish in the section How the GL proofs we’ll do translate to PA. The answer to your question is in that section. I use both the premises, because the GL implication using both the premises is sufficient to establish that if we have the PA theorem from the definition of Löbian fairness, then we must also have the PA theorem from the definition of Payorian fairness.
Yes, I agree that the GL derivation, with both of those premises, establishes that the Löbian FairBot cooperates at most as often as the Payorian FairBot is semantically a Payorian FairBot. But why are you allowed to have both premises? You don’t have both premises in the definition of either bot.
Edit: I think there are edge cases where the second premise does not hold, and so the Löbian FairBot might behave differently from the Payorian FairBot.
No, we’re not on the same page. You’re still repeating that we agree about the validity of the GL derivation.
The question is what the validity of the GL derivation implies about PA. What I’m saying is that the validity of the GL derivation implies that the Löbian FairBot (as defined in PA) satisfies the Payorian FairBot’s condition (as defined in PA). This works even though the GL derivation has two premises. That’s why I’m “allowed” to have both premises: because the validity of the GL derivation with two premises is sufficient for the desired conclusion about PA.
This is what I establish in the section How the GL proofs we’ll do translate to PA. Unless you either read that section and are convinced by it, or read that section and identify some mistake (there is none), how can this thread go anywhere?
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.
Right, I know the question isn’t whether the GL derivation is correct.
This is what I want to get on the same page about: do you agree that the GL derivation, with both those premises, establishes that the Löbian FairBot, as defined at the top of my post, must satisfy the condition of a Payorian FairBot, as defined at the top of my post?
This is what I establish in the section How the GL proofs we’ll do translate to PA. The answer to your question is in that section. I use both the premises, because the GL implication using both the premises is sufficient to establish that if we have the PA theorem from the definition of Löbian fairness, then we must also have the PA theorem from the definition of Payorian fairness.
Yes, I agree that the GL derivation, with both of those premises, establishes that the Löbian FairBot
cooperates at most as often as the Payorian FairBotis semantically a Payorian FairBot. But why are you allowed to have both premises? You don’t have both premises in the definition of either bot.Edit: I think there are edge cases where the second premise does not hold, and so the Löbian FairBot might behave differently from the Payorian FairBot.
No, we’re not on the same page. You’re still repeating that we agree about the validity of the GL derivation.
The question is what the validity of the GL derivation implies about PA. What I’m saying is that the validity of the GL derivation implies that the Löbian FairBot (as defined in PA) satisfies the Payorian FairBot’s condition (as defined in PA). This works even though the GL derivation has two premises. That’s why I’m “allowed” to have both premises: because the validity of the GL derivation with two premises is sufficient for the desired conclusion about PA.
This is what I establish in the section How the GL proofs we’ll do translate to PA. Unless you either read that section and are convinced by it, or read that section and identify some mistake (there is none), how can this thread go anywhere?
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.