> and that the second order axioms are not computably enumerable
He says that true sentences in second order logic aren't computably enumerable, he's not talking about the axioms.
> Don’t know if computably enumerable is the same as recursively enumerable
I've only ever seen them used as synonyms.
> Collect all true statements in this model of PA_2. Call that Super PA. That’s now my axiomatic system. I now have an axiomatic system that proves all true statements of arithmetic. Surely this set of axioms is not recursively enumerable.
What you call "Super PA" is called "the theory of PA". Its axioms are indeed not computably enumerable. That doesn't mean that the axioms of PA themselves aren't computably enumerable. And this much is true both for first and second order logic.
(edit: in fact, the set of Peano axioms isn't just computably enumerable, it's decidable - otherwise, it would be impossible to decide whether a proof is valid. This is at least true for FOL, but I do think it's also valid for SOL)
...it's decidable - otherwise, it would be impossible to decide whether a proof is valid.
Isn't that the whole issue with PA_2 vs. PA? In PA_2 with "full semantics" there is no effective procedure for determining if a statement is an axiom. In my mind this is what I mean by the incompleteness results not applying to PA_2. They do apply to Z_2 since that is an effective (computable?) system.
But Z2 is usually studied with first-order semantics, and in that context it is an effective theory of arithmetic subject to the incompleteness theorems. In particular, Z2 includes every axiom of PA, and it does include the second-order induction axiom, and it is still incomplete.
Therefore, the well-known categoricity proof must not rely solely on the second-order induction axiom. It also relies on a change to an entirely different semantics, apart from the choice of axioms. It is only in the context of these special "full" semantics that PA with the second-order induction axiom becomes categorical.
He says that true sentences in second order logic aren't computably enumerable, he's not talking about the axioms.
> Don’t know if computably enumerable is the same as recursively enumerable
I've only ever seen them used as synonyms.
> Collect all true statements in this model of PA_2. Call that Super PA. That’s now my axiomatic system. I now have an axiomatic system that proves all true statements of arithmetic. Surely this set of axioms is not recursively enumerable.
What you call "Super PA" is called "the theory of PA". Its axioms are indeed not computably enumerable. That doesn't mean that the axioms of PA themselves aren't computably enumerable. And this much is true both for first and second order logic.
(edit: in fact, the set of Peano axioms isn't just computably enumerable, it's decidable - otherwise, it would be impossible to decide whether a proof is valid. This is at least true for FOL, but I do think it's also valid for SOL)