FOM: 2nd order logic

[Harvey Friedman]

Both first order and second order logic provide languages for the
expression of mathematical statements.

First order logic is, in addition, a model for reasoning. And formal
systems based on first order logic also provide models for various kinds of
mathematical reasoning.

Second order logic is not itself a model for reasoning. And it cannot be
augmented to provide models for mathematical reasoning.

When it appears that second order logic is used as a model for reasoning,
what is really going on is that an associated system of first order logic
is constructed. Thus in reverse mathematics, we still speak of "second
order arithmetic," which is not a system based on 2nd order logic, but
instead a system based on first order logic which is associated with the
ideas of second order logic.

This is by far the best way that I know how to explain the crucial
difference. I am not happy with most of what has been said in this regard
on the FOM.

For instance, this way of looking at it handles the following kind of
idiotic position I once heard a rabidly anti-logic mathematician put
forward:

"There is no significance to the independence of the continuum hypothesis
from the axioms of ZFC. For after all, we know that the continuum
hypothesis is decidable in second order logic."

The point is that the Godel/Cohen stuff tells us something profound about
the limitations of (at least certain kinds of) mathematical reasoning,
because ZFC is used as a model of (certain kinds of) mathematical
reasoning. Whereas, second order logic tells us nothing of the kind, and is
not a relevant model of any kind of relevant mathematical reasoning.