[FOM] comment on the video of the lecture by Voevodsky at IAS

[Andre.Rodin at ens.fr]

> >> So he failed to inform his audience that the impossibility that Goedel
> >> actually established was the impossibility of proof-in-S of a sentence
> >> expressing the consistency of S, for any consistent and sufficiently
> >> strong system S.
> >


> So you too do not understand the sense of the  theorem. The above formulation
> is simply FALSE (and totally misleading).
>

I think that the most natural thing would be simply ask Voevodsky this question,
I'm sure he has interesting things to say about it. Why all these emotions (my
own included) instead of an arumentative talk?

Let me try to answer this question for Voevodsky (I have no idea, of course, if
Voevodsky's answer will be similar)>

Thesis:
Goedel has *proved* that there is no *proof-in-S* of a sentence
expressing the consistency of S, for any consistent and sufficiently
strong system S.

Question:
Does the notion of *proof-in-S* has anything to do with
the notion of *proof*, on which the mathematical community relies when it
reaches the consensus that Goedel indeed *proved* his theorem?

Here are two possible answers (I don't claim that my list of answers is
complete, there are more nuanced answers, of course).

1) NO, it has NOT. In that case the Goedel's result about *proof-in-S* has no
bearing on what mathematicians (including Goedel himself) prove and hence is
philosophically and foundationally unimportant.

2) YES, it has. The most straightforward version of this possible answer amounts
to ignoring the difference between *proof* (without qalification) and
*proof-in-S*. In this way  one gets the Goedel Paradox, which is
philosophically and
foundationally puzzling and forces people to think seriously about this matter.


To put forward a paradox and then investigate further details looking for a way
out is a well-established dialectical strategy (known since Plato) that forces
serious thinking. Voevodsky used it in the beginning of his talk. It is a
generous attitude to Goedel's work: he does take Godel seriously. Many - if not
most of - mathematicians assume 1), decide that the subject is irrelevant to
their work and leave it to fom specialists without ever listening what these
specialists are saying.


Hiding the problem by simple linguistic means like saying that Godel
*established* his result rather than saying that he *proved* it is a rhetoric
strategy that in fact supports 1). It does NOT promote a generous attitude to
Goedel's work.


Actually what Voevodsky further says in his lecture gives some substance to 1)
too.


> I think he has not done the effort to really understand it, or for
> ideological
> reasons has chosen to ignore/hide the real content (and sense) of the
> theorem.



What I particularly liked in his lecture is that, in my sense, it was completely
free from any ideology - very unlike most of what I read and hear elsewhere
about fom.


>  One can trust *nobody*.
>


Including you? All Cretans are liers.



Andrei

>