[FOM] Fwd: invitation to comment

[Andre.Rodin at ens.fr]

Dear Oran,



>I gather the theorem in question is meant as an example for a general
>point regarding the relation between a semi-formal proof in
>mathematics and its fully formalized counterpart. If I understand
>correctly, you're saying that there is a gap between the two, the
>closing of which is a matter of philosophy, or ideology (in the broad
>sense), rather than a matter of mathematics.


yes



>First, I'm not sure what sense of 'equivalence' is used here.

actually a broader term  like "adequacy" would be better to use here. I don't
know exactly what this relation of adequacy is or should be and I stress this
question as an open problem. I also observe that in the current practice of
formalization no good answer to this question is given, so this gap is filled
by some bold epistemic assumptions according to which formalization reveals the
nature of mathematical reasoning, makes is clearer, etc.


>To try
>to make this more concrete with an example: one way to read Hilbert's
>Programme and its formalism is as suggesting that we first map our
>target theory into a formal theory of a specific format, and then
>consider questions such as its consistency. This mapping is reversible
>- is this sufficient to conclude that there is _some_ kind of
>equivalence?

I also tend to think about formalization as a mapping. If such a map  would be
reversible it could be called equivalence in an appropriately specified sense.
But I cannot see that it is indeed reversible.  The reversibility condition for
maps, that I borrow from the elementary Category theory, is quite strong: map
m:A \rightarrow B is reversible iff there exists map n: A \leftarrow B such
that m and n cancel each other on BOTH sides (i.e. that the composition map m°n
equals A and the compositions map n°m equals B). The mere existence of a map
going in the opposite direction is sufficient only in case when there is at
most one map between two objects of our category. Why do you believe that
formalization is reversible? What about the fact that a formal theory may have
different models?

Using a mathematical notion of map (which in a category-theoretic setting is
more general than that of function) for treating formalization looks like an
attractive idea. However I see the following difficulty in it. A mathematical
map maps one mathematical object to another mathematical object. Formalization
maps a theory (not an object) to mathematical object. For this reason I don't
think that any mathematical notion of map - category-theoretic or other - can
really do the whole job. When I say that in  the "classical fom" there is a
speculative component I don't suggest that it can and should be eliminated by
some mathematical advances. I rather suggest that we need a better
philosophical work to be done here. In my view we need a *critical philosophy*
that takes seriously the current mathematical practice - rather than any
dogmatic philosophy or ideology that teaches mathematicians how to make
mathematics better than they do it.




>But at the same time it is clear that something is lost
>in this translation/mapping.



Yes


>If I may play on a double meaning of 'map' between a synonym for
>'function' and its meaning in non-technical contexts, Borges' point
>surely applies here, that a map in which nothing is lost would simply
>cover the entire region it maps, not being very helpful; and so, that
>a map loses some information is in the nature of mapping, and the only
>question is, is the map good for the purpose for which it is intended.
>There seems to me that if one considers this example, or some of
>Gödel's methods in proving the incompl. thms., there _is_ a clear
>mathematical test for the adequacy of the formalization chosen.


I wholly agree that useful maps "lose something". But I cannot understand what
"test for the adequacy of the formalization chosen" you have in mind. Could you
elaborate?


>To sum up: that something is lost in translation is clear. But what is
>it that you see as getting lost which is so essential as to make a
>semi-formal theory and its fully-formalized counterpart
>'non-equivalent'?


The main point where formal approaches fail is probably this: they fail to
account to how mathematics constructs (of forms) its objects. In my
(neo-Kantian) view the object-formation is an essential part of any
mathematical theory but not its preliminary. The only part of mathematics where
we have explicit rules of object-formation is the part of mathematics that
studies formal systems. Here we have explicit rules of building formulae and
systems of formulae. Saying that the whole of mathematics can be done formally
is tantamount to  saying that formulae are the only kind of objects that
mathematics really needs to take seriously. This idea is by no means crazy but,
 in my view, just wrong. In any event mathematics as it is practiced today
doesn't take this idea as its regulative principle.  And I try to take this
fact about today's mathematical practice seriously.

Andrei