Whoops! I said in the OP that the precursor to A (before diagonalization) is a recursive function, but it’s not. It’s not computable because it has to check whether several propositions are theorems of Peano arithmetic, and also because of that existential quantifier in the definition of A. If A itself were recursive, then it would provably (in PA) cooperate or defect; but it cooperates or defects unprovably (in PA). I’ll edit the OP to make it correct.
The rest of the post still works because all the functions are representable — they can be represented by formulas in arithmetic — even if they’re not recursive. Thanks for bringing this to my attention.
EDIT: Oy, they’re not even “representable” in the technical sense. They’re only definable.
The agent described in the OP is definitely not a Turing machine that halts.
Hmm. The agent is a recursive function, so it is equivalent to a Turing machine that halts, no?
But I see your point. There is no simple formula, so if nothing else, it’s inelegant.
Whoops! I said in the OP that the precursor to A (before diagonalization) is a recursive function, but it’s not. It’s not computable because it has to check whether several propositions are theorems of Peano arithmetic, and also because of that existential quantifier in the definition of A. If A itself were recursive, then it would provably (in PA) cooperate or defect; but it cooperates or defects unprovably (in PA). I’ll edit the OP to make it correct.
The rest of the post still works because all the functions are representable — they can be represented by formulas in arithmetic — even if they’re not recursive. Thanks for bringing this to my attention.
EDIT: Oy, they’re not even “representable” in the technical sense. They’re only definable.