If PA is the system the agent uses, then by “the proof system,” I mean PA. I was speaking generically, in case you’d prefer to use ZFC or PA + Con(PA) or whatever.
If the algorithm finds a proof that defection is better, it defects, period.
Er, are you saying that as soon as the algorithm finds such a proof, it stops searching and returns “defect”? That will not work, because then the Löbian reasoning won’t go through, for the reason cousin_it gave. [Because PA cannot prove Con(PA), it also cannot prove that “there’s a short proof that cooperate is better” implies “the agent cooperates”—for all PA knows, PA might be inconsistent, and there might be an even shorter proof that defect is better.]
Or do you mean that the algorithm looks through the whole list of proofs, and if it never finds a proof that cooperate is better, it defects? Then we’re in agreement; I was simply pointing out that in this case, we know that if the algorithm proves “defect is better,” then it will not cooperate, because we know that PA is consistent, so if the algorithm proves “defect is better” then it will not prove “cooperate is better.”
Because PA cannot prove Con(PA), it also cannot prove that “there’s a short proof that cooperate is better” implies “the agent cooperates”
It can enumerate all shorter proofs, and see if any of them imply a different action of the agent. (Note that PA is reflexive, that is can prove that any given finite set of its statements is logically consistent.)
Can you give some link or citation about “reflexive”? I can’t figure out what this means. It seems to me that if PA can prove every finite subset of its axioms consistent, then it can prove itself consistent: “If PA is inconsistent, then there would be a statement A and a proof of A and a proof of NOT A; but each proof only uses a finite set of axioms; the union of two finite sets is finite; so there is a finite set of axioms of PA that proves both A and NOT A; but every finite subset of PA is consistent, contradiction. Ergo, PA is consistent.” Clearly, I’m misunderstanding something.
(PA can’t talk about sets in general, but finite sets are fine, and “finite subset of PA” just means “finite set of propositions, all of which are in the enumeration that is PA.”)
It can’t prove that every finite set of its statements is consistent, but for every finite set of its statements it can prove its consistency. (See this chapter, Corollary 8.)
I don’t understand. The relevant step in the argument, as far as I understand it, requires an inference from “there exists a proof in n steps that cooperate is better” to “the agent cooperates”. It seems to me that “enumerating all shorter proofs” would requiring knowing the precise proof (or at least its length), not just the statement “there exists such a proof”. But I’m probably not following what, exactly, you have in mind; could you expand on your argument?
[I should say I was wrong to say “it … cannot prove that” above—all I can say is that one particular technique for showing that it can prove it doesn’t go through.]
The setting is sufficiently confusing at this point that I give up (I’m not sure what we are talking about). I’ll try to work on a proof (not the proof) of something along the lines of this conjecture.
for all PA knows, PA might be inconsistent, and there might be an even shorter proof that defect is better.
If the agent checked all proofs of length less than X, and none of them prove statement T, there are no proofs of T shorter than X, even if the theory is inconsistent and T is provable (therefore, by longer proofs).
If PA is the system the agent uses, then by “the proof system,” I mean PA. I was speaking generically, in case you’d prefer to use ZFC or PA + Con(PA) or whatever.
Er, are you saying that as soon as the algorithm finds such a proof, it stops searching and returns “defect”? That will not work, because then the Löbian reasoning won’t go through, for the reason cousin_it gave. [Because PA cannot prove Con(PA), it also cannot prove that “there’s a short proof that cooperate is better” implies “the agent cooperates”—for all PA knows, PA might be inconsistent, and there might be an even shorter proof that defect is better.]
Or do you mean that the algorithm looks through the whole list of proofs, and if it never finds a proof that cooperate is better, it defects? Then we’re in agreement; I was simply pointing out that in this case, we know that if the algorithm proves “defect is better,” then it will not cooperate, because we know that PA is consistent, so if the algorithm proves “defect is better” then it will not prove “cooperate is better.”
It can enumerate all shorter proofs, and see if any of them imply a different action of the agent. (Note that PA is reflexive, that is can prove that any given finite set of its statements is logically consistent.)
Can you give some link or citation about “reflexive”? I can’t figure out what this means. It seems to me that if PA can prove every finite subset of its axioms consistent, then it can prove itself consistent: “If PA is inconsistent, then there would be a statement A and a proof of A and a proof of NOT A; but each proof only uses a finite set of axioms; the union of two finite sets is finite; so there is a finite set of axioms of PA that proves both A and NOT A; but every finite subset of PA is consistent, contradiction. Ergo, PA is consistent.” Clearly, I’m misunderstanding something.
(PA can’t talk about sets in general, but finite sets are fine, and “finite subset of PA” just means “finite set of propositions, all of which are in the enumeration that is PA.”)
It can’t prove that every finite set of its statements is consistent, but for every finite set of its statements it can prove its consistency. (See this chapter, Corollary 8.)
I don’t understand. The relevant step in the argument, as far as I understand it, requires an inference from “there exists a proof in n steps that cooperate is better” to “the agent cooperates”. It seems to me that “enumerating all shorter proofs” would requiring knowing the precise proof (or at least its length), not just the statement “there exists such a proof”. But I’m probably not following what, exactly, you have in mind; could you expand on your argument?
[I should say I was wrong to say “it … cannot prove that” above—all I can say is that one particular technique for showing that it can prove it doesn’t go through.]
The setting is sufficiently confusing at this point that I give up (I’m not sure what we are talking about). I’ll try to work on a proof (not the proof) of something along the lines of this conjecture.
If the agent checked all proofs of length less than X, and none of them prove statement T, there are no proofs of T shorter than X, even if the theory is inconsistent and T is provable (therefore, by longer proofs).