So you modify the agent so that line 3 says “cooperating is provably better than defecting” and line 4 says “defecting is provably better than cooperating”. But line 3 comes before line 4, so in proving Conjecture 4 you’d still have to show that the condition in line 3 does not obtain. Or you could prove that line 3 and line 4 can’t both obtain; I haven’t figured out exactly how to do this yet.
Well the agent definition contains a series of conditionals. You have as the last three lines: if “cooperating is provably better than defecting”, then cooperate; else, if “defecting is provably better than cooperating” then defect; else defect. Intuitively, assuming the agent’s utility function is consistent, only one antecedent clause will evaluate to true. In the case that the first one does, the agent will output C. Otherwise, it will move through to the next part of the conditional and if that evaluates to true the agent will output D. If not, then it will output D anyway. Because of this, I would go for proving that line three and 4 can’t both obtain.
Or you could prove that line 3 and line 4 can’t both obtain; I haven’t figured out exactly how to do this yet.
How about this? Suppose condition 3 and 4 both obtain. Then there exists and a and b such that U(C) = #a and U(D) = #b (switching out the underline for ‘#’). Also, there exists a p and q such that p > q and U(D) = #p and U(C) = #q. Now U(C) = #a > #b = U(D) = #c > #q = U(C) so U(C) > U(C). I may actually be confused on some details, since you indicate that a and b are numbers rather than variables (for instance in proposition 2 you select a and b as rational numbers), yet you further denote numerals for them, but I’m assuming that a >b iff #a > #b. Is this a valid assumption? I feel as though I’m missing some details here, and I’m not 100% sure how to fill them in. If my assumption isn’t valid I have a couple of other ideas. I’m not sure if I should be thinking of #a as ‘a’ under some interpretation.
Going a little bit further, it looks like your lemma 1 only invokes the first two lines and can easily be extended for use in conjecture 4 - look at parts 1 and 3. Part 1 is one step away from being identical to part 3 with C instead of D. ~Con(PA) → ~ Con(PA + anything), just plug in Con(PA) in there. Adding axioms can’t make an inconsistent theory consistent. Getting the analogous lemma to use in conjecture 4 looks pretty straightforward—switching out C with D and vice versa in each of the parts yields another true four part lemma, identical in form but for the switched D’s and C’s so you can use them analogously to how you used the original lemma 1 in the proof of proposition 3.
So you modify the agent so that line 3 says “cooperating is provably better than defecting” and line 4 says “defecting is provably better than cooperating”. But line 3 comes before line 4, so in proving Conjecture 4 you’d still have to show that the condition in line 3 does not obtain. Or you could prove that line 3 and line 4 can’t both obtain; I haven’t figured out exactly how to do this yet.
Well the agent definition contains a series of conditionals. You have as the last three lines: if “cooperating is provably better than defecting”, then cooperate; else, if “defecting is provably better than cooperating” then defect; else defect. Intuitively, assuming the agent’s utility function is consistent, only one antecedent clause will evaluate to true. In the case that the first one does, the agent will output C. Otherwise, it will move through to the next part of the conditional and if that evaluates to true the agent will output D. If not, then it will output D anyway. Because of this, I would go for proving that line three and 4 can’t both obtain.
How about this? Suppose condition 3 and 4 both obtain. Then there exists and a and b such that U(C) = #a and U(D) = #b (switching out the underline for ‘#’). Also, there exists a p and q such that p > q and U(D) = #p and U(C) = #q. Now U(C) = #a > #b = U(D) = #c > #q = U(C) so U(C) > U(C). I may actually be confused on some details, since you indicate that a and b are numbers rather than variables (for instance in proposition 2 you select a and b as rational numbers), yet you further denote numerals for them, but I’m assuming that a >b iff #a > #b. Is this a valid assumption? I feel as though I’m missing some details here, and I’m not 100% sure how to fill them in. If my assumption isn’t valid I have a couple of other ideas. I’m not sure if I should be thinking of #a as ‘a’ under some interpretation.
Going a little bit further, it looks like your lemma 1 only invokes the first two lines and can easily be extended for use in conjecture 4 - look at parts 1 and 3. Part 1 is one step away from being identical to part 3 with C instead of D.
~Con(PA) → ~ Con(PA + anything), just plug in Con(PA) in there. Adding axioms can’t make an inconsistent theory consistent. Getting the analogous lemma to use in conjecture 4 looks pretty straightforward—switching out C with D and vice versa in each of the parts yields another true four part lemma, identical in form but for the switched D’s and C’s so you can use them analogously to how you used the original lemma 1 in the proof of proposition 3.
Yep, this sounds about right. I think one do has to prove “#a > #b if a > b”, or rather