[FOM] Remedial mathematics?

[Timothy Y. Chow]

On Mon, 23 May 2011, Jeremy Shipley wrote:
> Existentialism (Frege): Existence (ie, intuition of logical and
> geometric objects) precedes essence (ie, consistent axiomatic
> systemization).
> 
> Essentialism (Hilbert): Essence precedes existence.
[...]
> it strikes me as odd that fom practitioners should appeal to 
> existentialism, even if it is accepted in ordinary mathematical 
> reasoning. I would have thought that even if ordinary mathematics is 
> existentialist, most fom practitioners would be essentialist. Otherwise 
> why care about consistency proofs in the first place, which find their 
> relevance, or at least their historical motivation, within an 
> essentialist program?

Part of the problem here is that you're anachronistically lifting an old 
debate into the modern world.  In the old days, it wasn't so clear that 
every mathematical argument could be easily formalized in a variety of 
ways, nor was it clear that we couldn't hope for a finitary proof of the 
consistency of infinitary set theory.  F.o.m. practitioners may in the 
past have looked to consistency proofs as providing a road from deep 
skepticism about infinitary reasoning to absolute certainty in its 
legitimacy, but thanks to Goedel they now recognize that as a chimera.  
They are therefore frustrated when mathematicians who ought to know better 
continue to cling to the old way of thinking, insisting that the only way 
to "know for sure" that some system is consistent is to give a finitary 
proof of it, while simultaneously failing to practice what they preach 
(since mathematicians continue to claim to "know for sure" lots of things 
without any finitary proof).

Getting back to your question, I do not think that f.o.m. practitioners 
are "appealing to existentialism."  They simply recognize that the 
"trivial proof" of the consistency of PA that I sketched can be formalized 
in ZF (for example), and don't worry about it further.  ZF is stronger 
than PA, but so what?  Again, that should bother you only if you think 
there's something illegitimate about infinitary reasoning and retain a 
craving for a finitary proof of the consistency of PA.  Neither the 
existence of a finitary proof of the consistency of PA, nor the 
consistency of PA itself, is considered an interesting mathematical 
problem any more, because the issues are well understood.

*Relative* consistency of various formal systems is still interesting from 
a f.o.m. perspective because they help us paint a picture of the landscape 
of formal systems and where they stand relative to each other.  But f.o.m. 
practitioners no longer regard consistency proofs as functioning as 
definitive refutations of skeptical doubts.

Tim