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

[Curtis Franks]

> Date: Tue, 17 May 2011 11:48:50 +0200
> From: Andre.Rodin at ens.fr
> To: fom at cs.nyu.edu
> Subject: Re: [FOM] comment on the video of the lecture by Voevodsky at IAS
>
>> 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?


Professor Voevodsky began his talk by pointing to the slide in question 
and saying that what he had written is not literally what Goedel proved, 
would probably strike a lot of people as too strong, etc., but that in 
his forthcoming remarks he would try to explain why he thinks this 
strong formulation is warranted by considerations of the broader situation.

Parts of that explanation were very surprising. For example, one would 
expect the "third option" in the later slide to be something like "PA is 
for all we know inconsistent." That seems to be what follows from the 
denial of 1 and 2. But Voevodsky repeatedly suggests the stronger claim: 
We have here some evidence that PA is probably inconsistent --or -- the 
inconsistency of PA is the most likely explanation of Goedel's theorem. 
It seems to me that Ed Nelson draws roughly this same inference. It was 
also surprising that he associated Goedel's own attitude with option 1 
(there must be some way around the theorem) rather than with option 2 
(we know that PA is consistent without proof). Another surprise: given 
Goedel's work, the only reasons to believe in the consistency of PA are 
"transcendental" (doesn't Voevodsky agree to pragmatic justification of 
computational procedures, etc?) Well, there were many such surprises. 
But it's much more surprising to me to read discussion of this matter on 
this list proceed as if Voevodsky had not offered any explanation and 
had not acknowledged the difference between what Goedel proved and what 
he was saying.

Kuhn had a famous line: "When reading the works of an important thinker, 
look first for the apparent absurdities in the text and ask yourself how 
a sensible person could have written them. When you find an answer ... 
then you may find that more central passages, ones you previously 
thought you understood, have changed their meaning."

Surely at the heart of this matter is Andre Weill's quip: "Gentzen 
proved the consistency of arithmetic, i.e., induction up to the ordinal 
omega, by means of induction up to epsilon_0." It is not hard to get 
oneself in the mindset that a proof of the consistency of PA, if it is 
to be of use for foundational purposes, should not use the consistency 
of "some stronger system" as a background assumption. I have to image, 
from what
Voevodsky said in this lecture, that this is the sense in which he takes 
Godel's work to have shown that there can be no proof of the consistency 
of PA or of stronger systems. One can have that attitude and still think 
that lots of strong mathematical statements can be proved: One shows 
that they follow from usual mathematical principles, using usual 
mathematical techniques. Voevodsky just doesn't think that this 
interpretation of Gentzen's proof could fulfill the familiar 
foundational aspirations.

One has to wonder exactly what point Voevodsky's univalent foundations 
is supposed to have, given that he presumably doesn't share those 
familiar foundational aspirations. (He happily cites the pragmatic 
justification of ordinary mathematical activity as reason to take the 
possibility of inconsistency of PA in stride.) This isn't a dismissal of 
his project. It is hard not to be interested in what new conceptions of 
foundations our best mathematicians are working with.

By the way, Gentzen's proof should be amendable to the analysis in 
homotopic type theory, just like any other proof.

Curtis