FOM: second-order logic is a myth -- also, informal versus formal reasoning

[Randall Holmes]

In this note, I discuss Simpson's claim that

"mathematics can be formalized in ZFC"

This is a very common claim; I often make it myself (more often I
claim that mathematics can be formalized in strong extensions of NFU,
a claim to which the same strictures apply that I apply below to the
commoner claim about ZFC).  It is true in a certain practical sense.
But I think that there are also good grounds (which most of us know
about, though I will tiresomely summarize them below) for the contrary
claim that

"arithmetic (and so most of mathematics) cannot be formalized at all".

This is relevant to the thread about second-order logic because I
think that the use of "naive" and "informal" by Simpson in contexts
where Black (apparently) and I (certainly) would say that second-order
logic is being used are indicative of the contrasting viewpoints at
work.

The informal view of arithmetic is "second-order" from my standpoint
and involves an appeal to "naive theory of sets" from Simpson's.  In
any event, from either standpoint, one can arrive at the conclusion
that the axioms and rules of inference of first-order PA are correct
for reasoning about the natural numbers.

We now encode terms and proofs of first-order PA by natural numbers, so
that we can (apparently) talk about formal proofs in PA inside PA
itself.

We can refer to open sentences with one natural number parameter as
"formal predicates of a natural number" and enumerate these.

We can define a formal predicate which ostensibly expresses:

"the nth formal predicate of natural numbers cannot be proved to hold of n"

This is the mth formal predicate for some natural number.

We can then express the G\"odel sentence as (roughly):

"the mth formal predicate of natural numbers holds of m"

>From an informal standpoint, we can see that this is true; it says
(informally) that it itself cannot be proved.  If it could be proved,
then (informally) we would be able to prove a false sentence in PA,
which we know from our informal standpoint is not the case.

However, since it can't be proved, there are models of PA in which it
is false.  In these models, there are "natural numbers" which encode
"proofs" of the G\"odel sentence.  These must be nonstandard natural
numbers, since there aren't actually any such "proofs".

It is usually said that the G\"odel sentence is self-referential.  I
claim that this is not what is really happening.  The reason that
logical disaster (paradox) is averted here is precisely that
self-reference cannot be achieved: the axioms of PA do not succeed in
specifying the natural numbers exactly, and so do not succeed in
specifying the notion of "formal proof in PA" precisely either; the
only reason that we see self-reference is that we informally accept
the notions formalized in PA at "face value" as equivalent to the
corresponding informal notions.

In true second-order arithmetic, it is possible to define such notions
as "formal proof in first order PA" exactly; in fact, "formal proof in
T", where T is any formal system, can be defined precisely in
second-order arithmetic.  The argument given above can be adapted in
the true second-order context to prove that there can be no such
notion as "formal proof in second-order arithmetic".

This applies to the formal system usually called "second-order
arithmetic" as well; certain principles which I accept because I
accept true second-order arithmetic are formalized in this first-order
two-sorted theory.  But at the informal level I accept even stronger
statements as true which are not provable in this formal system: for
example, I informally accept the truth of the G\"odel sentence
of the formalized "second-order arithmetic" or even stronger systems
(such as ZFC).

My claim here is that the informal standpoint cannot be eliminated.  I
can extract formal principles of reasoning which I regard as correct
from my informal standpoint and work inside such a formal system, but
such a formal system never exhausts the mathematical principles that I
accept as correct.  For any such system T, since I accept T as valid,
I accept Con(T) as valid as well (for example; this sort of thing is
presumably not restricted to the G\"odel phenomenon!).

It may be that my informal standpoint can be completely formalized,
but if so it cannot be formalized by me; I will not accept this
hypothetical formalization as capturing my informal convictions even
if it is presented to me (I presumably won't understand it).  I do
accept PA (and ZFC) so these theories cannot be formalizations of
mathematics as I understand it.  Since Simpson accepts these systems,
they can't formalize mathematics as he understands it, either :-)

I think that this issue of the relationship between our informal
understanding of mathematics and our formalizations is a crucially
important one for the topic of this list.  It also may help to clarify
the sense in which I (and perhaps others) regard second order logic as
indispensible and distinct from the "second-order theories" which can
be formalized.  

Note: I don't regard second-order principles (which are necessarily
informal, though partially formalizable) as exhausting informal
principles of reasoning, or even as exhausting the informal principles
needed for the discussion above.

disclaimer: I don't profess that anything in this posting is original
with me (except of course any errors or infelicities).

And God posted an angel with a flaming sword at | Sincerely, M. Randall Holmes
the gates of Cantor's paradise, that the       | Boise State U. (disavows all) 
slow-witted and the deliberately obtuse might | holmes at math.idbsu.edu
not glimpse the wonders therein. | http://math.idbsu.edu/~holmes