[FOM] second-order logic once again
mongre at gmx.de
Wed Sep 5 06:20:42 EDT 2012
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
More information about the FOM