[FOM] shipman's challenge: the best defense

[catarina dutilh]

From: Vladimir Sazonov: 
"Adequate formalization" is not the same as 
"adequate translation" from one natural language to another (or from a 
natural language to formal) as it might be thought. 

I would like to hear more on why it is so (I'm not intrinsically opposed to this view, but I think arguments are required to back this claim). 

If I understand Vladimir's views correctly, informal mathematical intuitions are not mathematics properly speaking. THerefore, for him there is no such thing as 'formalizing' ordinary mathematics, as ordinary mathematics as he understands it is already thoroughly formalized. In other words, there is nothing to be formalized in the first place. This is on the one hand an empirical claim (which can be assessed by simply looking at mathematical textbooks and other sources of canonical, 'normal' mathematics in the Kuhnian sense), but on the other hand it is a conceptual issue of demarcation. What is to count as mathematics? I am not a practicing mathematician myself, but I know many mathematicians who are much more lax in their understanding of what is to count as mathematics. So while Vladimir's is an interesting view of mathematics as an enterprise, it is a contentious view that is (I think) far from being unanimously accepted among mathematicians as well
 as philosophers of mathematics. His considerations on the Formalization Thesis (basically that it is trivially true) all hinge on this particular view of mathematics. 

Vladimir, if it's not too much to ask, I would appreciate if you could comment on the following passage from a very interesting paper by Wang (in Mind 1955):

"Consider, for example, an oral sketch of a newly discovered proof, an abstract designed to communicate just the basic idea of the proof, an article presenting the proof to people working on related problems, a textbook formulation of the same, and a presentation of it after the manner of Principia Mathematica. The proof gets more and more thoroughly formalized as we go from an earlier version to a later. […] Each step of it should be easier to follow since it involves no jumps." (Wang 1955, 227) 

One could take the formalization even further, and, from the presentation of the proof ‘after the manner of Principia Mathematica’, construct an even more detailed presentation of it using lambda-calculus, for example. 

The question is then: at which point does the proof (argument) in question become a *mathematical* proof as Vladimir understands them? 

Catarina


      ____________________________________________________________________________________
Never miss a thing.  Make Yahoo your home page. 
http://www.yahoo.com/r/hs