I think you’re reading too much into what I’m saying. I’m not suggesting that second order arithmetic is useful as a mathematical framework to talk about reasoning, in the way that first-order logic can. I’m saying that second order arithmetic is a useful way to talk about what makes the natural numbers special.
I’m also not suggesting that second order arithmetic has anything deep to add relative to a naïve (but sufficiently abstract) understanding of induction, but given that many people don’t have a sufficiently abstract understanding of induction, I think it usefully illustrates just how broadly induction has to be understood. (To be clear, I’m also not suggesting that second order arithmetic is the one true way to think about the natural numbers, only that it’s a useful perspective.)
Consider a non-logician mathematician to whom the induction principle is not primarily a formal statement to be analyzed, but just, well, induction, a basic working tool. Given a large proof as you describe, ending in an application of induction. What would be the benefit, to the mathematician, of viewing that application as happening in second-order logic, as opposed to first-order set theory? Why would they want to use second-order anything?
I’m not claiming there is any such benefit. This is the wrong question to ask; neither Eliezer’s original post nor my comment were written for an audience of mathematicians concerned with the optimal way to do mathematics in practice.
Let G be the arithmetical statement expressing the consistency of ZFC. There are models of set theory in which G is true, and models in which G is false. Are you saying that second-order arithmetic gives us a better way, a less ambiguous way, to study the truth of G?
No, I am not saying that.
The way I see it, different models of set theory agree on what natural numbers are, but disagree on what subsets of natural numbers exist.
If there are models where G is true and models where G is false then different models of set theory don’t agree on what natural numbers are.
This ambiguity is not resolved by second-order arithmetic; rather, it’s swept under the carpet. The “unique” model “pinpointed” by it is utterly at the mercy of the same ambiguity of what the set of subsets of N is, and the ambiguity reasserts itself the moment you start studying the semantics of second-order arithmetic which you will do through model theory, expressed within set theory. So what is it that you have gained?
No, the ambiguity is not resolved by second-order arithmetic. The ambiguity is not resolved by anything, so that doesn’t seem like a very useful objection.
Also, note that I didn’t refer to either a unique model nor to pinpointing. (I’m aware that Eliezer did, but you’re replying to me.) What I said was:
“[S]econd order arithmetic gives us a universal way of picking the natural numbers out in any situation. Different models of set theory may end up disagreeing about what’s true in the natural numbers, but second order arithmetic is a consistent way of identifying the notion in that model of set theory which lines up with our intuitions for the what the natural numbers are”
I think you’re reading too much into what I’m saying. I’m not suggesting that second order arithmetic is useful as a mathematical framework to talk about reasoning, in the way that first-order logic can. I’m saying that second order arithmetic is a useful way to talk about what makes the natural numbers special.
I’m also not suggesting that second order arithmetic has anything deep to add relative to a naïve (but sufficiently abstract) understanding of induction, but given that many people don’t have a sufficiently abstract understanding of induction, I think it usefully illustrates just how broadly induction has to be understood. (To be clear, I’m also not suggesting that second order arithmetic is the one true way to think about the natural numbers, only that it’s a useful perspective.)
I’m not claiming there is any such benefit. This is the wrong question to ask; neither Eliezer’s original post nor my comment were written for an audience of mathematicians concerned with the optimal way to do mathematics in practice.
No, I am not saying that.
If there are models where G is true and models where G is false then different models of set theory don’t agree on what natural numbers are.
No, the ambiguity is not resolved by second-order arithmetic. The ambiguity is not resolved by anything, so that doesn’t seem like a very useful objection.
Also, note that I didn’t refer to either a unique model nor to pinpointing. (I’m aware that Eliezer did, but you’re replying to me.) What I said was: “[S]econd order arithmetic gives us a universal way of picking the natural numbers out in any situation. Different models of set theory may end up disagreeing about what’s true in the natural numbers, but second order arithmetic is a consistent way of identifying the notion in that model of set theory which lines up with our intuitions for the what the natural numbers are”