What useful results or proofs use the higher order expressiveness in higher logic?

Question

According to this article

Quine has criticized higher-order logic (with standard semantics) as "set theory in sheep's clothing". Quine's criticism focuses on the lack of an effective, sound, complete proof theory; he argues that this makes HOL not a "logic". Shapiro has responded to this criticism, arguing that the additional semantic expressiveness can offset the lack of a proof theory, and arguing that a "logic" need only have a deductive system or a semantical system, but perhaps may not have both.

a. Why does Quine say "set theory in sheep's clothing"?

I tend to agree with Shapiro on the tension between deductiveness & expressiveness.

b. But are there useful results which naturally use the higher-order expressiveness either in their proof or statement, apart from the categoricity of 2-logic as opposed to 1-logic.

Since higher logic with Henkin semantics reduces to typed 1-logic it seems essential to keep full semantics.

Answer 1

The idea is that, in set theory, one is developing a formal language to talk about sets. In particular, one is quantifying over sets in set theory. Second-order logic, when it introduces predicate variables, seems to be doing something very similar, since the interpretation of these predicates is meant to be a set. You can't quantify over sets of sets in second-order logic, but as you ascend into higher and higher orders, you come closer and closer to set theory. Quine's objection, then, is that second-order "logic" isn't a logic at all: it's a restricted theory of sets.

If you want to learn more about these things, you really ought to read Shapiro's book Foundations without Foundationalism, which is a fantastic introductory source for both the technical and philosophical material regarding second-order logic. I would also suggest looking at Quine's thoughts on these things in Philosophy of Logic. Boolos also has some interesting articles defending (monadic) second-order logic philosophically as a kind of plural logic (i.e. a logic with plural terms).

With regard to using second-order logic in mathematics, you might want to look into the field of reverse mathematics which deals a lot with second-order PA (I don't know much about it myself). The issue of finding proofs that use second-order logic is a bit tricky, as I understand it, since when you do want to use second-order logic, you can often just get away with using first-order set theory.