Second-order logic does have a computable definition of provability, it’s just that the logic is incomplete under that definition. It may be disconcerting to work with an incomplete logic, since you know there are universal truths you can’t prove even before you get to a particular theory and its consequences.
In general, using SOL to pinpoint the truths of natural numbers doesn’t seem like an appealing idea:
Actual interesting mathematical content about N is provable in FOL PA, and if not, the natural place mathematicians go to is set theory.
The second-order induction axiom can be formalized in first-order set theory. At least set theory is explicit about the fact that the notion of “all subsets” is somewhat vague; SOL seems to sweep that under the carpet.
By the time you proved categoricity of SOL PA, you’ve used natural numbers with full induction in your naive meta-theory, and are inextricably dependent on that pre-formal naive understanding of what natural numbers are.
Second-order logic does have a computable definition of provability, it’s just that the logic is incomplete under that definition. It may be disconcerting to work with an incomplete logic, since you know there are universal truths you can’t prove even before you get to a particular theory and its consequences.
In general, using SOL to pinpoint the truths of natural numbers doesn’t seem like an appealing idea:
Actual interesting mathematical content about N is provable in FOL PA, and if not, the natural place mathematicians go to is set theory.
The second-order induction axiom can be formalized in first-order set theory. At least set theory is explicit about the fact that the notion of “all subsets” is somewhat vague; SOL seems to sweep that under the carpet.
By the time you proved categoricity of SOL PA, you’ve used natural numbers with full induction in your naive meta-theory, and are inextricably dependent on that pre-formal naive understanding of what natural numbers are.