Do you have a reference for the second order induction schema being recursively enumerable? My understanding - I’m not a logician - is that the second order Peano Axioms are categorical. The Incompleteness theorems don’t apply to this system since the axioms are not recursively enumerable. The second order Axioms are different than second order Arithmetic.
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.