[FOM] mathematics as formal

catarina dutilh cdutilhnovaes at yahoo.com
Sun Mar 9 09:11:54 EDT 2008

catarina dutilh wrote:
> There are two related but independent issues here: one issue is when
> mathematics became formal in OUR sense(s) of formal (e.g. mechanically
> checkable proofs, among others); the other issue, and the one I'm
> interested in at the moment, is when mathematics began to be seen
> as formal, in THEIR (i.e. past mathematicians and philosophers of
> mathematics) sense(s) of formal.

Vaughan Pratt wrote:
A third issue (or issues 3-5 depending on how one counts) that seems to 
me to be separate from the above two is the extent to which formality 
bears on each of the nature, practice, and foundations of mathematics. 

This is most certainly a very important distinction in this context. I am not sure whether I am comfortable with the idea of 'the nature of mathematics': even if there is such a thing, it is so elusive (and perhaps subjective) that it is nearly impossible to talk about it. But distinguishing practice and foundations, as well as mathematical practice vs. philosophy of mathematics (a related but not equivalent distinction) is certainly very important. One thing is what people actually do, another thing is what they (and others) think they are doing (it doesn't necessarily coincide).
As has been pointed out several times before on this list, the point of view of people working on foundations of mathematics, i.e. attempts to axiomatize the whole of mathematics, mainly with logical tools, is in many senses very different from the point of view of practicing mathematicians. In the former, concern with formality is arguably much more significant than in the latter.
So in a sense (and rephrasing my original distinction), mathematics has never become 'formal', as actual practices in current mathematics are (and perhaps always will be) by and large 'informal' in one sense or another. Mathematical practice, now as well as in the past, displays enough heterogeneity so as not to allow for global qualifications such as the one implied in my original phrasing of the distinction. On the other hand, it is possible (whether it is informative, it's a different matter) to look at a mathematical theorem of the past, or the work of a specific mathematician, and deem that it satisfies many of the criteria that WE usually associate with the notion of 'formal' (for example, mechanically checkable proofs), even if the author himself (alas, virtually no women here!) did not use this term to describe his own approach.
But this was of course not my original query, which concerned when and with whom the explicit attribution of a formal character to mathematics first came about. (Btw, many thanks to Panu Raatikainen, who pointed out that Frege criticizes 'formalists' already in his Grundlagen, which must mean that something like the idea that mathematics is, or can be reduced to, a formal system was already in the air before Hilbert). I am particularly interested in the historical development of the very concept of 'formal', and naturally the explicit association of this concept to mathematics is an important chapter of the story. Hence my query.
Going back to the distinction proposed by Vaughan Pratt: the fact that there is such a distinction between mathematical practice and foundational work does not (should not!) mean that either of them is more important vis-a-vis the other. To my mind they are equally important, and in many senses complementary enterprises. In fact, the tradition of foundations of mathematics has become a branch of mathematical practice in itself -- which was in some sense what Hilbert had intended all along. 

Be a better friend, newshound, and 
know-it-all with Yahoo! Mobile.  Try it now.  http://mobile.yahoo.com/;_ylt=Ahu06i62sR8HDtDypao8Wcj9tAcJ 

More information about the FOM mailing list