Strict formalism

[Timothy Y. Chow]

In my Mathematical Intelligencer article on the consistency of arithmetic, 
I introduced the term "strict formalism."  Recently, I came up with a way 
to present my point about strict formalism in a particularly vivid manner. 
Suppose someone says they're a formalist and suggests that the consistency 
of PA is an open problem.  Here is my reply.

Consider the following "formal system" which I will call Z.  Z has just 
one axiom: "0" (i.e., a string of length one, comprising a single numeral, 
0).  It also has just one rule of inference:

   if "x" is a theorem then so is "x0"

So for example, "00" is a theorem, "000" is a theorem, and so on.  Now I 
present the following conjecture.

   Conjecture. "1" is not a theorem.

In other words, the string of length one, comprising a single numeral, 1, 
cannot be obtained from the axiom of Z by any finite number of 
applications of the rule of inference.

The above Conjecture might seem ridiculous.  However, I claim that for the 
strict formalist, not only is the Conjecture non-trivial---it remains an 
open problem.  A strict formalist can play the Z game and can verify, on a 
case-by-case basis, that "00" is a theorem and "000" is a theorem, and so 
forth.  However, to conclude that "1" is not a theorem requires 
*mathematical reasoning about abstract objects* which a strict formalist 
is not entitled to.

If a formalist claims to *know* that the above Conjecture is true, then 
the burden of proof is on the formalist to articulate precisely, and 
defend, the principles---which of necessity must go beyond the principles 
of strict formalism---according to which he or she is able to arrive at 
that conclusion.

Tim