[FOM] Fwd: invitation to comment

[Andre.Rodin at ens.fr]

> If I haven't exhausted your patience yet, I am wondering what,
> according to this point of view, would change if someone were to
> establish a reversal for the Poincare conjecture, in the sense that
> over some weak base theory, the Poincare conjecture implies Con(PA).
>
> (I have no intuition for whether or not this is even possible in the
> case of the Poincare conjecture... but for the sake of argument, one
> might admit the possibility that *some* acceptedly "mathematical"
> result *might* eventually be shown to imply Con(PA) over a weak base
> theory.)

In order to establish such a result you need first of all to *formalize* the
Poicare-Perelman theorem PP  (I can see no reason to call it conjecture any
longer), that is, replace PP by its formal counterpart FPP. Similarly for any
other acceptedly mathematical result. Here in my view is the core problem. From
a mathematical viewpoint formal propositions and formal theories are
mathematical *objects* like points, spaces, fields, numbers and whatnot. (I was
very glad to hear a similar statement from Voevodsky in his video.)  One may
prove  about these things mathematical theorems  like "formal proposition P
implies formal proposition Con(X) over the base formal theory B". I take such
theorems to be mathematical theorems proper on equal footing with PP. But at
this point mathematics ends and the following speculative arguments is put
forward: FPP *represents* or *expresses* PP in such a way that studying
properties of FPP (which is an object!) one may come to know something
essential about PP. This speculative assumption is often strengthen by saying
that PP as it stands is somewhat unclear and that FPP clarifies the content of
PP.
My guess is that such an assumption is not justified. Just think how different
are PP and FPP. FPP is a pulpable combinatorial (syntactic) object; one can
play with it like with elementary geometrical constructions. This is where the
sense of precision and clarity comes from. But what this object has to do with
PP which is a *theorem* but not a mathematical object, about which one may
prove this or that theorem?
FPP likely implies Con(PA) over some weak base formal theory B. So if PA is
in-consistent FPP is false. This does not imply that PP is false and that
Perelman's argument is  flawed.
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.

This is my take on the problem. Hence the following answers to your questions:

>
> 1. Would the proof of the Poincare conjecture (or some substitute)
> cease to be regarded as a mathematical proof proper?

YES

>
> 2. Would the proof come to be regarded as involving philosophical
> speculation or non-mathematical assumptions?
>
NO

> or conversely:
>
> 3. Would the proof of Con(PA), via the Poincare conjecture (or some
> substitute) come to be regarded as a purely mathematical result?
>

NO because such a proof involves formalisation of PP, which is not a purely
mathematical procedure. (a mathematical procedure does something with
mathematical objects while formalisation turns a theory into an object).
> or alternatively:
>
> 4. Would this point of view regard it as inconceivable that it will
> ever be shown that the Poincare conjecture (or any "mathematical"
> substitute) implies Con(PA), because the Poincare conjecture has a
> mathematical proof, while according to this point of view, Con(PA) can
> never have a purely mathematical proof?

it can be *shown* in some general sense but not proved mathematically (because
of the need of  formalisation).
>
Andrei