[FOM] shipman's challenge: the best defense

[Vladimir Sazonov]

Catarina Dutilh (CD):

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).

VS:

"adequate translation" from one natural language to another assumes 
that both represent something sufficiently vague, and we want to to say 
"the same" in another language, if possible. (For example, I still do 
not know the adequate English translation of the Russian word schast'e 
- what a person experiences may be once in the life, if at all 
possible. This is typically and, I think, non-adequately translated as 
happiness. "Are you happy?" is similar to "Do you feel yourself 
comfortably?". However, I am not a linguist and feel the English not so 
well.)

The process of formalization, as I wrote in a recent posting, 
inevitably assumes developing the initial vague idea so that it even 
disappears and we get instead a couple:

new (now a mathematical) idea + its formalization,

and it is this couple which is mutually adequate. We hardly can say 
that new formalism is adequate to the old idea at least because it has 
"disappeared" and changed so radically.


CD:

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.


VS:

Of course, everything depends on the context, which in our case, is 
related with which philosophy of mathematics to admit. I admit 
Formalist View on Math (FVM), and therefore start behaving accordingly. 
Like in the context of writing a mathematical paper we become rather 
unusually behaving (writing, arguing) from the point of view of a man 
from the street, e.g.

I consider FVM as the most clear, consistent and scientific. It is a 
very realistic view assuming the real world, our thought (including ANY 
kind of intuitions and imaginations) and formal tools (formal systems) 
to be invented and studied by mathematicians to make our thought 
stronger. (Recall, e.g. opening a planet by calculations based on the 
formal tools in Analysis, including physical lows written on the formal 
language of Analysis. Like a miracle!)


Of course, from the everyday point of view on mathematics I would not 
be so over-scrupulous. I can accept that informal mathematical 
intuition (where formal ingredients are not seen at the first sight) is 
indeed mathematical. But in the above context, I can discuss things 
only on the base of FVM, and then I would say differently: informal 
mathematical intuition alone, if taken outside corresponding (adequate) 
formalization, is not mathematics properly speaking. Mathematical 
intuition cannot exist alone (like content cannot exist outside of its 
form, like an animal cannot survive without its skeleton). The formal 
"skeleton" of our mathematical intuition may be immediately invisible, 
but it can be revealed, may be with some thought efforts and a bit of 
imagination. However, if we have some amoeba-like skeleton- or 
form-free intuition then it is not mathematical yet. Just 
blah-blah-blah.

CD:

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?

VS: I believe that this is most important question without a good 
answer to which we would have a lot of various, may be witty opinions, 
but hardly converging to somewhere. (Like the known parable on elephant 
and several blinds.)

FVM puts formal (= rigorous) side of mathematics forward because this 
is THE ONLY feature which distinguishes mathematics from anything else. 
Say, abstract thought and intuition, appealing to the real world exist 
virtually in human any activity. The rigour is related ONLY to 
mathematics. As soon as we see some elements of rigorous reasoning in 
any kind of human activity we easily treat this as some attempt of 
mathematization. FVM absolutely does not reject mathematical intuition 
and imagination as somebody intends to ascribe this point of view to 
FVM. It rather relates them with with formalisms. This view on 
mathematics is highly general. It does not restrict mathematics to 
"numbers and figures" or anything like that (say, to sets or categories 
and functors, etc). ANY intuition based on or supported by a formalism 
is mathematical. (Of course it should be said much much more on the 
specifics and peculiarities of relation between mathematical intuition 
and formalisms.)


CD:

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.


VS:

Yes, of course. The point is that FVM is not well understood yet by the 
mathematical community. It is rather AWFULLY WRONGLY understood, even 
here in FOM.


CD:

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.

VS:

I am not sure why have you mentioned lambda-calculus. Why it gives 
anything "more detailed". Take ZFC. It is represented as a formal 
system for which it is no problem to write a computer program verifying 
ZFC-proofs. Thus, presentation of any mathematical proof in ZFC is as 
detailed as could be imagined. However, I would call the formal system 
ZFC as low level (like the language of Turing Machines can be 
considered as low level programming language). I guess that Mizar or 
other systems mentioned in this discussion can be treated as a higher 
level version of ZFC. The point is that writing formal proofs (like 
writing computer programs) should be more human friendly task.

But, from the point of view of working mathematicians writing a 
rigorous proof does not mean EXPLICIT writing an absolutely formal 
text. Mathematical texts rather contain convincing arguments (from 
which it follows for some formally inclined readers) that some 
fragments of this text can be POTENTIALLY "transformed" into an 
EXPLICITLY formal proof.

(Note that there is some problem how to understand "potentially". Is 
the resulting explicitely formal proof feasible or not? Projects like 
Mizar are devoted, as I understand, to demonstrate that affirmatively 
assuming that appropriate high level versions of formalisms is used. I 
consider the question of feasibility highly important. This can be a 
source for further clarification or may be ramification of our 
undesrtanding of mathematical rigour.)

CD:

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

VS:

At the moment when an expert reader confirmed that the proof is 
POTENTIALLY formalizable. That is, strictly speaking, ANY ordinary 
mathematical text is rather a DRAFT of a proof or a construction, etc. 
Only in the process of its reading and rereading it becomes (confirmed 
to be) a POTENTIAL mathematical proof. Only people working on Mizar 
project or the like make a mathematical draft to be EXPLICITLY 
mathematical proof.

I absolutely do not intend to say anything slighting about what I call 
mathmatical drafts. All mathematics is written down in such drafts. I 
only suggest some terminological and conceptual distinctions.

The above is written according to the contemporary standard of 
mathematical rigour. Even old mathematical results are considered 
nowadays according to this standard. Of course, in the older times 
other standards were used. But is not it highly instructive that 
virtually everything rigorous/mathematical according to these old 
standards satisfies to the new contemporary standard of POTENTIAL 
formalizability. Does not it mean that even ancient mathematicians, 
most typically Euclid, worked instinctively towards creating the 
contemporary formal standard? Because FORMALLY GROUNDED THOUGHT is (and 
always was) the real nature of mathematics.


I hope I clarified my views. (Unfortunately, many things were 
essentially repeated with variations from previous postings.)

Best wishes,


Vladimir Sazonov

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.