[FOM] Fwd: invitation to comment

[Oran Magal]

Dear Andrei,

Could I trouble you for a clarification? You wrote:

> In order to claim that FPP is equivalent to PP people use various
> non-mathematical arguments. I cannot imagine a *mathematical* argument that
> could fill this gap.
>

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.

First, I'm not sure what sense of 'equivalence' is used here. 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? But at the same time it is clear that something is lost
in this translation/mapping.

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. And
yet, of course something is lost; indeed, the 'meaning' of the terms
involved, including even the most basic logical connectives, is
_deliberately_ lost, otherwise formalization would not yield anything
to work with.

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'? This is not a critique, just a question. I'm a
beginner in these topics, so I apologize if my question is too naive
or just a misunderstanding.

Yours,

Oran Magal
McGill University