"I started to post a comment, but it got long enough that I’ve turned my comment into a blog post."
So the study of second-order consequences is not logic at all; to tease out all the second-order consequences of your second-order axioms, you need to confront not just the forms of sentences but their meanings. In other words, you have to understand meanings before you can carry out the operation of inference. But Yudkowsky is trying to derive meaning from the operation of inference, which won’t work because in second-order logic, meaning comes first.
... it’s important to recognize that Yudkowsky has “solved” the problem of accounting for numbers only by reducing it to the problem of accounting for sets — except that he hasn’t even done that, because his reduction relies on pretending that second order logic is logic.
I think this critique undervalues the insight second order arithmetic gives for understanding the natural numbers.
If what you wanted from logic was a complete, self-contained account of mathematical reasoning then second order arithmetic is a punt: it purports to describe a set of rules for describing the natural numbers, and then in the middle says "Just fill in whatever you want here, and then go on". Landsburg worries that, as a consequence, we haven't gotten anywhere (or, worse, have started behind where we started, since no we need an account of "properties" in order to have an account of natural numbers).
But, thanks to Gödel, we know that a self-contained account of reasoning is impossible. Landsburg's answer is to give up on reasoning: the natural numbers are just there, and we have an intuitive grasp of them. This is, obviously, even more of a punt, and the second order arithmetic approach actually tells us something useful about the concept of the natural numbers.
Suppose someone produces a proof of a theorem about the natural numbers---let's say, for specificity, they prove the twin primes conjecture (that there are infinitely many twin primes). This proof proceeds in the following fashion: by extensive use of the most elaborate abstract math you can think of---large cardinals and sheafs and anabelian geometry and whatnot---the person proves the existence of a set of natural numbers P such that 1) 0 is in P, 2) if x is in P then x+1 is in P, and 3) if x is in P then there are twin primes greater than x.
Second order arithmetic says that this property P must extend all the way through the natural numbers, and therefore must itself be the natural numbers, and so we could conclude the twin primes conjecture.
The rest of this proof is really complicated, and uses things you might not think are valid, so you might not buy it. But second order arithmetic demands that if you believe the rest of the proof, you should also agree that the twin primes conjecture holds. This is actually worth something: it says that if you and I agree about all the fancy abstract stuff, we also have to agree about the natural numbers. And that's the most we can ask for.
To phrase this differently, second 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. That's a very different account than the one offered by first order logic, but it's a valuable one in its own right.
One more phrasing, just for thoroughness. Landsburg passes off an account of the natural numbers to Platonism: we just intuit the natural numbers. But suppose you and I both purport to have good intuitions of the natural numbers, but we seem to disagree about some property. So we sit down to hash this out; it might turn out that we have some disagreement about what constitutes valid mathematical reasoning, in which case we may be stuck. But if not---if we agree on the reasoning---then eventually the disagreement will boil down to something like this:
You: "And since 0 is turquoise and, whenever x is turquoise, x+1 is also turquoise, all the natural numbers are turquoise."
Me: "Wait, those aren't all the natural numbers. Those are just the small natural numbers."
You: "What? What are the small natural numbers?"
Me: "You know, the initial segment of the natural numbers closed under the property of being turquoise."
You: "There's an initial segment of the natural numbers which includes 0, is closed under adding 1, but isn't every natural number?"
Me: "Sure. The small natural numbers. Haven't you heard of them?"
You: "Wait, are there any initial segments of the small natural numbers which include 0 and are closed under adding 1?"
Me: "Sure. The tiny natural numbers, for starters."
You: "Look, you're using the word 'natural numbers' wrong. It means..." and then you explain the second order induction axiom. So apparently whatever I thought was the natural numbers was some other bizzarre object; what the second order induction axiom does for a Platonist is pin down which Platonic object we're actually talking about.
I disagree with your example:
But set theory says the same thing. And set theory, unlike second-order arithmetic, is probably strong enough to formalize the large and complicated proof in the first place. Even if there are elements in the proof that go beyond ZFC (large cardinals etc.), mathematicians... (read more)