[FOM] comment on the video of the lecture by Voevodsky at IAS
cfranks at nd.edu
Wed May 18 17:28:55 EDT 2011
> 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,
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
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.
More information about the FOM