[Date Index] [Thread Index] [FOM Postings] [FOM Home]

*To*: fom@math.psu.edu*Subject*: FOM: Hilbert's Program and complexity*From*: detlefsen.1@nd.edu*Date*: Wed, 3 Nov 1999 07:10:46 -0600*Sender*: owner-fom@math.psu.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.

[Date Prev] [Date Next] [Thread Prev] [Thread Next]

[Date Index] [Thread Index] [FOM Postings] [FOM Home]