"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 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)

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 t... (read more)