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.
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.