[FOM] Convincing Edward Nelson that PA is consistent

[Timothy Y. Chow]

On Wed, 20 Jun 2018, Arnon Avron wrote:
> In your posting you refer to two types of people: the skeptical 
> formalists (who are somehow more reasonable than the strict formalists) 
> and the ultrafinitists. I understand from your message that Nelson was 
> both. But *should* an ultrafinitist be a (skeptical) formalist? 
> Conversely: *Should* a skeptical (or even strict) formalist be an 
> ultrafinitist? If so - why? If not - how would you convince a very 
> skeptical formalist who is not an ultrafinitist that PA is consistent?

First let me try to be a bit more careful about what the terms "skeptical 
formalist" and "ultrafinitist" mean.

"Ultrafinitist" presumably should mean someone who objects to concepts 
such as "arbitrarily long finite string" or "arbitrarily long finite 
proof."

"Skeptical formalist" presumably should mean someone whose primary view of 
mathematics is that it is a game played with formal symbols, and that much 
mathematical discourse should not be interpreted as being *meaningful*. 
But if the formalist is not "strict" then it means that the formalist 
accepts *some* mathematical statements and arguments as being meaningful 
and correct.  To repeat my most basic example, anyone but a strict 
formalist would agree that if you repeatedly apply the rule "prepend an S" 
to the symbol "0" then you will never get a string with some symbol other 
than S or 0 in it.

To convince a very skeptical formalist who is not an ultrafinitist that PA 
is consistent---well, that may not be possible.  Since he or she is not an 
ultrafinitist, that at least means that there is some hope that some 
conventionally defined formal system such as PRA will capture a (proper) 
subset of the arguments that the skeptical formalist accepts.  Then it is 
just a matter of assessing whether that system is strong enough to prove 
Con(PA).  If the skeptical formalist won't accept any system that is 
strong enough to prove Con(PA), then there's no hope of convincing him or 
her that PA is consistent.

As for what someone *should* believe---I don't think that any of these 
views entails any of the others.  For example, you could be an 
ultrafinitist and still think that mathematicians have access to absolute 
truths about finite abstract objects such as natural numbers, or affirm 
that mathematics is a sociological construct rather than a formal game. 
Conversely, a strict formalist might not be a "card-carrying" 
ultrafinitist---although a strict formalist only ever manipulates 
syntactic objects of feasible size and so the question of what a strict 
formalist does with infeasibly large objects just "doesn't come up."

Tim