[FOM] shipman's challenge: the best defense
Vladimir Sazonov
Vladimir.Sazonov at liverpool.ac.uk
Mon Jan 14 16:34:07 EST 2008
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.
More information about the FOM
mailing list