FOM: Re: Hilbert's program and complexity

[Matthew Frank]

On Nov. 3, Mic Detlefsen gave the following quote from Hilbert, and asked
some questions about it and "inventional complexity":

"Our formula game that Brouwer so deprecates has, besides its mathematical
value, an important general philosophical significance. For this formula
game is carried out according to certain definite rules, in which the
technique of our thinking is expressed. These rules form a closed system
that can be discovered and definitively stated. The fundamental idea of my
proof theory is none other than to describe the activity of our
understanding, to make a protocol of the rules according to which out
thinking actually proceeds."  (van Heijenoort, p. 475)

Here I think Hilbert made a mistake.  I do not think that our thinking
particularly proceeds according to rules, much rules which can be stated
definitively and circumscribed in some formal system.  So I think the
"Hilbert's program" expressed in this paragraph could be interpreted as
having two goals:

1) describing the activity of our understanding, the way in which our
(mathematical) thinking actually proceeds.  In doing this proof theory
would be largely irrelevant; one would instead embark on a project like
that of Polya or Lakatos, and one would want to consider how we think
about ideal elements.  A notion of inventional complexity would also be
relevant.  (Can we measure this now?  Perhaps.  We do say things like:
"that is a deep proof" or "I could have done that myself", etc.)

2) describing formula games in which various theorems can be derived.  I
would interpret proof theory in this way (and agree with Hilbert that it
is important).  For this we do not need a precise metric of inventional
complexity--which is good because no such metric seems to be available. 

Detlefsen also asked:  "If 'reverse' proofs should, on (some kind of)
average, turn out to be significantly more difficult to discover than
their 'non-reverse' counterparts, wouldn't the 'surprising brevity and
elegance' that Hilbert took to be the special virtue of 'classical'
reasoning be largely lost or at least compromised?"

Consider the proofs of various theorems within the various subsystems of
second-order arithmetic.  (The question about the other type of "reverse
proofs", e.g. of WKL_0 or ACA_0 from mathematical statements + RCA_0,
doesn't seem particularly relevant here.)  Surely, we sacrifice a great
deal of brevity and elegance when we translate our usual proofs into this
(or any other) framework.  On the other hand, the conservation results
that we can get for theorems proved within these frameworks are a way of
establishing the epistemological virtues of classical mathematics that
Hilbert so wanted to establish, and I think Hilbert would have liked them
(particularly the constructive proofs of the conservation results).

--Matt Frank