[FOM] second-order logic once again

[Robert Black]

Let me try again.

There's a position one might call ‘ultraformalism’: mathematical truth 
consists only in the truth of constructively proved sigma_1 sentences of 
the form 'there is a (number which codes a) proof of ... in the ... 
system, for here it is'. At least one of Bourbaki's brains seems to have 
thought this. To see how silly it is, note that in formal arithmetic the 
first theorem we prove is the associativity of addition. But the 
ultraformalist doesn't believe the associativity of addition: he only 
believes that the associativity of addition is provable (in PA, say). 
So, in advance of doing the calculation, he has no reason to believe 
that, say, (123+345)+678 = 123+(345+678). He should be surprised every 
time something like this works out. Of course the calculation will have 
to turn out that way if PA is consistent, but the ultraformalist doesn't 
believe that PA is consistent, but only that its consistency can be 
proved (say in ZF). And he doesn't believe that ZF is consistent ... . 
And since he doesn't think any universally quantified arithmetical 
statement can be true, he had better just give up on trying to give an 
account of applied mathematics.

Then there's a position we could call just 'formalism': arithmetical 
sentences quite generally have truth values, and thus so do sentences 
about the provability *or unprovability* of sentences in formal systems. 
But the sentences in formal systems going beyond arithmetic (analysis, 
set theory) have no meaning and no truth value, it's all just a game 
with meaningless symbols and only the *metatheory* is true. I think this 
view is almost as silly as ultraformalism, and it has a problem with 
explaining what mathematics beyond arithmetic is for and how it can be 
applied, but however that may be, note that on this view *the 
completeness theorem for first-order logic is not true or even 
meaningful: all that is true is that it is provable in (say) ZF*. 
Similarly, the incompleteness of second-order logic is not true but only 
provable. On this view semantics is all meaningless anyway and there is 
nothing special about first-order logic.

But my question wasn’t addressed to ultraformalists or formalists, but 
to those who think it is *true* (and not just provable in some formal 
system) that there are complete proof procedures for first-order logic 
but that there aren’t for second-order logic, and who conclude from this 
(by an argument which I don't accept, but never mind that) that the 
notion of second-order validity is not determinate. My problem is: once 
you've got to your conclusion, can you still state the premise?

The tempting move now is to say that different models of first-order ZF 
have different sets of 'second-order validities', but that in every such 
model the 'set of second-order validities' is not r.e., and that's a 
statement of incompleteness that doesn't assume the determinacy of 
second-order logic, since everything is relativized to models. But I 
think it does assume the determinacy of second-order logic in its naïve 
quantification over *all* models of first-order ZF (of which, of course, 
the fattest ones will be initial segments of the models of genuinely 
second-order ZF).

Robert