https://mathoverflow.net/questions/97077/z-2-versus-second-o...
In the following mathoverflow answer Nik says,
These are fundamental questions. We know that any computable set of axioms which holds of the natural numbers must also have nonstandard models.
The second order Peano Axioms are not computable since those axioms are categorical.
https://mathoverflow.net/questions/332247/defining-the-stand...
Are you of the opinion that mathematics is computer science? I have a hard time believing that the Jacobian Conjecture is computer science.
https://en.wikipedia.org/wiki/Second-order_arithmetic#The_fu...
An other equivalent option would be to use the language of second order logic, where you only need a finite amount of axioms, because the comprehension scheme is already included in the rules of second order logic. This one is PA_2.
Since these definitions do not refer to anything uncomputable such as mathematical truth, both systems are clearly recursively enumerable. This means that Gödel's incompleteness theorem applies to both, in the sense that you can define a sentence in the language of arithmetic that is unprovable in Z_2 or PA_2, and whose negation is also unprovable.
All of these considerations have little to do with models or categoricity, which are semantic notions. I think your confusion stems from the fact that model theorists have the habit of using a different kind of semantics for Z_2 (Henkin semantics) and PA_2 (full semantics). Henkin semantics are just first order semantics with two sorts, which means that Gödel's completeness theorem applies and there are nonstandard models. Full semantics, on the other hand, are categorical (there is only one model), but this has nothing to do with the axioms not being recursively enumerable -- it is just because we use a different notion of model.
PS: I certainly do not consider mathematics to be included in computer science. Even though as a logician, I have been employed in both mathematics departments and computer science departments...
https://math.stackexchange.com/questions/4753432/g%C3%B6dels...
Andreas Blass in the comments says that the Incompleteness results don’t apply to the second order Axioms (tabling about PA_2 here and not Z_2) and that the second order axioms are not computably enumerable. Maybe that’s the correct concept I was remembering from mathematical logic class. Don’t know if computably enumerable is the same as recursively enumerable but given what you’ve said I’m guessing they are different notions.
Consider the standard model of ZFC. Assume ZFC is consistent. Within this model there is one model of PA_2. 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.
Full semantics, on the other hand, are categorical (there is only one model), but this has nothing to do with the axioms not being recursively enumerable -- it is just because we use a different notion of model.
If those axioms were recursively enumerable then the Incompleteness theorems would apply, right?
What Noah Schweber says here seems pertinent:
https://math.stackexchange.com/questions/4972693/is-second-o...
On the other hand, proof theorists and computer scientists are perfectly happy to use proof systems for second order logic which are not complete. In that case, there are many effective proof systems, and given that the axioms of PA_2 are recursively enumerable (they are in finite number!), Gödel's incompleteness will apply.
If you are still not convinced, I encourage you to decide on a formal definition of what you call PA_2, and what you call a proof in that system. If your proof system is effective, and your axioms are recursively enumerable, then the incompleteness theorem will apply.
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)
Incompleteness does apply to second order arithmetic (it applies to every logical system that contains first order PA), but due to different reasons: second order logic doesn't have a complete proof calculus. "Second-order PA is categorical" means that there is only one model of second-order PA, that is, for every sentence P, either PA2 |= P or PA2 |= not(P), but you'll still have sentences P such that neither PA2 |- P nor PA2 |- not(P) - and for "practical" purposes, the existence of proofs is what matters.
Andreas Blass in the comments says that Incompleteness does not apply to PA_2.
https://math.stackexchange.com/questions/4753432/g%C3%B6dels...
A complete proof system needs to be able to derive Γ |- φ for every pair Γ, φ such that Γ |= φ. Not just when Γ is the complete theory of some structure. Completeness of first-order logic (and its failure for second-order logic) is about the logical system itself, while the incompleteness theorems are about specific theories - people often mix these up, but they talk about very different things.
> Andreas Blass in the comments says that Incompleteness does not apply to PA_2.
He says something rather different, namely that its "meaningless". That's a value judgement. Incomplete proof calculi for second order logic do exist (e.g. any first-order proof calculus) and for those, what I wrote is true. Andreas Blass would probably just think of this as an empty or obvious statement.
