FOM: Hilbert's Program and complexity

[detlefsen.1@nd.edu]

Herewith a few remarks to complement the interesting postings that Harvey,
Matthew Frank, Panu Rattikainen, Jeremy Avigad and others have made over
the past few days. Its purpose is to call attention to what I think is a
distinction between two fundamentally different types of complexity that
seems not to have been observed in the literature on proof theory generally
and seems not to have entered thus far into the exchanges here on FOM. The
distinction is best introduced with a few prefatory references to Hilbert
and his understanding of proof theory.

Describing his proof theory, Hilbert wrote:

"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. Thinking, it so happens, parallels speaking and
writing: we form statements and place them on behind another. If any
totality of observations and phenomena deserves to be made the object of a
serious and thorough investigation, it is this one ..." Foundations of
Mathematics, p. 475 (van Heijenoort)

Hilbert elaborated this basic idea in various other remarks. He said, for
example, that (i) use of the classical principles of logical reasoning was
particularly central and important to our thinking, that thinking has been
conducted in accordance with them ever since thinking began (vH., 379),
that (ii) reasoning which proceeds in accordance with them is 'especially
attractive' (vH., 476) because of its 'surprising brevity and elegance'
(ibid.), that (iii) taking classical logical reasoning away from the
mathematician, would be like taking away the telescope from the astronomer
and depriving the boxer the use of his fists (in somewhat less passionate
prose 'we cannot relinquish the use ... of any ... law of Aristotelian
logic ... since the construction of analysis is impossible without them'
(l.c., 471)).

Hilbert thus believed that there are certain patterns of thinking that are
less complex (more efficient) than others. The type of complexity he seems
to have had in mind, however, is what I would (and have, in a 1990 paper
and elsewhere) referred to as 'inventional complexity' ... that is,
roughly, the complexity of the thinking involved in DISCOVERING or
INVENTING A PROOF NOT GIVEN TO THE PROVER.

I would (have) contrast(ed) this type of complexity with what I call
'verificational complexity' ... that is, again roughly, the complexity of
the thinking involved in DETERMINING OF A GIVEN OBJECT WHETHER OR NOT IT IS
A PROOF (of a given proposition).

Question 1: What kind of complexity are Harvey et al. talking about? Is it
inventional or verificational complexity?

My answer: I think it is, for the most part, verificational complexity. In
order to determine the inventional complexity of a proof, it seems, at
least on the face of it, that one must do more than count symbol
occurrences. Perhaps, in the end, we'll see that even inventional
complexity can be measured as (some function of) symbol-occurrence
complexity ... but, from what we now know, the 'order of invention', if you
will, is not the order of symbol-occurrence complexity (or any obvious
transformation of it).

Caution: Inventional and verificational complexity are not entirely
independent of one another, of course. In particular, inventional
complexity seems to subsume verificational complexity in this sense: in
order to discover something AS a proof that thing must be seen to be a
proof ... in other words, it must be VERIFIED to be a proof. Hence, every
discoved proof is verified as a proof.

Still, though not independent of one another, the two do not seem to be
remotely equivalent in terms of their complexity. In particular, the task
of verifying of a given object that it is a proof is typically strictly
easier than to discover a proof for a given proposition.

This raises the following questions ...

Question 2: To carry out Hilbert's Program (and/or related programs such as
Reverse Mathematics) and to evaluate the success of attempts at doing so,
don't we ultimately have to make use of a notion of and metric for
inventional complexity? (2a) For example, 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? (2b) If this
were the case, could reverse mathematics rightly be described and/or
thought of as a modification or partial realization of Hilbert's Program?
(2c) Do we have a plausible way of measuring or even of recognizing the
inventional complexity of 'reverse' proofs?

and

Question 3: Is there any notion of complexity in present-day proof theory
that is plausible as a means of measuring inventional complexity?

Note: To the more philosophically minded, let me say that, as a
philosopher, I take these questions (i.e. questions relating to the
preservation of Hilbert's Program) very seriously. (That will probably
strike some of you as a laughable understatement.) I do so because I think
that any philosophically satisfying foundation for mathematics will have to
cope successfully with the main 'phenomenon' of mathematical thinking that
Hilbert's finitism struggled with ... namely, the justification of the many
striking uses of so-called 'ideal' elements in the history of mathematics.
I thus believe that it's vitally important to save Hilbert's Program ... or
some modification of it.

Let me close by asking a question designed to help us begin thinking about
'inventional' complexity ... or at least one particular variety of it.

The efficiencies brought about by the use of ideal elements were famously
expressed by Gergonne in the form of his so-called 'dualities'. These
allowed one to convert a proof of one theorem into a proof of its dual by a
simply process of substitution. Between duals, then, there is something
that might be called a 'proof form': duals have the same proof form, and
conversion of this common form into a proof is a matter of executing a
scheme of substitutions.

Question 4: Does this give the basic model for understanding the
efficiencies brought about by the introduction of ideal elements generally?
Or does it only work this way in some cases? That is, should we try to
develop an analysis that proceeds in terms of 'proof forms'?

Question 5: Is there an even more general type of form of thinking--a
'theory form', if you will--that ought to brought into focus and used in
our analysis of mathematical reasoning? Hilbert wrote to Frege in a letter
of Dec 29, 1899 that:

"... it is surely obvious that every theory is only a scaffolding or schema
of concepts together with their necessary relations to one another, and
that the basic elements can be thought of in any way one likes. ... any
theory can always be applied to infinitely many systems of basic elements
... [this] can never be a defect in a theory, but is rather a tremendous
advantage ..."

Note: Much later (in his 1930 Koenigsberg address) Hilbert made the same
point in connection with a certain formal convergence he had noticed (I've
never known exactly what this formal convergence is) between the Euclidean
axioms for linear congruence, on the one hand, and the laws determining the
coupling of traits in deviant offspring of Drosophila. He described this
convergence as more 'wonderful' than anything 'imagined in even the boldest
fantasy'.

Hilbert thus seems to have thought--and, indeed (as I have argued
elsewhere), this was the core of anything that deserves to be called his
'formalist' position--that there is something like a 'theory-form' or a
realm of theory-forms--a family of thought-forms that apply pervasively to
ALL areas of human thought. These are forms that are so general that (in
contrast to the dualities), they facilitate transfer or transformation of
knowledge not only from one mathematical subject-area to another, but,
indeed, transfer/transformation of knowledge from a mathematical area to a
non-mathematical area through some type of process of 'substitution'. More
than anything else, Hilbert's formalism (and his related proof theory)
seems to have been an acknowledgement or and quest for these 'mother
structures' of all (systematic) thinking.