FOM: formalism

[Robert Black]

Matthew Frank:

>I am a formalist, in that I believe:  1) it is essential to modern
>mathematics that it can be formalized, and 2) for much of modern
>mathematics the only meaningful notion of truth (if it is a notion of
>truth at all) is provability in some formal system.

I don't think anyone on this list is likely to quarrel with (1), but if one
starts pressing (2) (and disregards the let-out 'much of') I think it
starts to fall apart. Bourbaki says something closely related (_Theorie des
Ensembles_ I,22) when he says that the claim that some sentence is not a
theorem of a formal system 'can have no sense *in mathematics*' (Bourbaki's
emphasis).

When we prove a sentence S in a formal system, if all we take ourselves to
be really doing is announcing that it is so provable, then we are always
announcing a sigma_1 result, whatever the logical complexity of S, and our
proof of that result is of course constructive; we have exhibited the
(Goedel numer of the) array of dried ink which is a proof of S. So this is
really the view that all mathematical knowledge consists of constructively
proved sigma_1 results.

Consider now a pi_1 claim like 'PA is consistent'. What is the 'formalist'
going to say about this claim? He can of course announce that it's
provable, in, say, ZF (a sigma_1 fact), or that it's disprovable in, say,
PA+not-Con(PA) (another sigma_1 fact), but what about the claim itself's
being true or false?

There seem to be two options:

Either: You say it's not the sort of thing that could be true. I find this
pretty zany, particularly because it could (for all we know) be false! Do
you really want to go down this road? Is the claim meaningless though its
negation is meaningful? Or do it and its negation suddenly become
meaningful only if the negation turns out to be true? Or is it meaningful
but couldn't be true though it could be false???

Or: You say that it probably is true, but the claim that it's true is not
*mathematical*. (Is this Bourbaki's let-out?) But then what on earth is the
name of the branch of human intellectual endeavour to which that claim
*does* belong? Perhaps universities should open up some departments for
this new subject!

Robert

Robert Black
Dept of Philosophy
University of Nottingham
Nottingham NG7 2RD

tel. 0115-951 5845