Nowadays, I guess, a lot more people are sympathetic to the idea that second order logic is real logic than in Quine’s day due to the popularity of plural logic. However, this falls short of full second order logic by quite a long way due to the fact that it can’t quantify over relations. For example, you can’t state various facts about sizes or the axiom of choice.

In the first order case, the question seems to be more tractable. If we identify the logical vocabulary as those terms that are not sensitive to the particular identities of the individuals (i.e. whose extensions remain unchanged if you permute the domain) then we get the cardinality quantifiers and arbitrary unions of the cardinality quantifiers as logical terms. McGee confirms the intuition that these truly are logical by showing that the permutation invariant (first order) vocabulary are precisely those defineable from intuitively logical operations: negation, identity, arbitrary conjunctions, universal quantification with respect to an arbitrary block of variables. Admittedly, this language () is not a language that anyone can speak, but that is a deficiency on our part, and should not place constraints on logic. Thus, first order quantification seems to be ontologically innocent, even for quantifiers like ‘there are uncountably many F’s’.

Indeed, similar results hold if we allow second order quantifiers. They are also permutation invariant, and conversely, the permutation invariant second order quantifiers is precisely those that can be defined in the equivalent of with arbitrary blocks of second order quantifiers too. But the difference here, it seems, is that it is not clear that second order quantification over relations is ontologically innocent. Sure, plural quantifiers are, but as soon as we leave the realm of monadic quantification there is less reason to think so (although some have suggested that you can get around it: e.g. Burgess, and Rayo and Linnebo.)

Anyway, I was wondering if it would be possible to reduce second order quantification to first order quantification in our infinitary language. If this were possible then we could happily use the second order quantifiers and safely know that the are not ontologically committing, because they are definable using first order vocabulary.

I think you can do it, but I’m not entirely sure so this might be wrong. Let be antizero – the size of everything. For each second order variable *X* of the language keep aside many variables: for . Then define a translation schema as follows: [UPDATE: I reformulated it slightly so that it wasn’t quite so confusing.] For a subset of the domain, I, we define the translate of with repsect to I as follows:

For the other connectives and quantifiers translation just commutes in the natural way. A couple of notes: this isn’t like in that it must allow truly arbitrary disjunctions and quantifications (including proper class length conjunctions.) Secondly, it’s not really as simple a translation as it looks because in the first clause I left *I* “free”, to be later “bound” by an earlier application of the second translation clause. What this really means is that the length of the disjunction in the first clause is really determined by when it is called in the second clause. Lastly – that’s just monadic quantification, which we already had – but it seems it will extend nicely to polyadic second order quantifiers (this time we disjoin instead.)