[FOM] partial transcript: Voevodsky on Gentzen's proof

[meskew at math.uci.edu]

Dear all,


I thought Voevodsky's remarks on Gentzen's proof were strange.  Here are
his words verbatim:

<<So these combinatorial objects are called ordinals less than \epsilon_0.
 And one can give a definition what does it mean for two ordinals to be
one less than another. And that's all quite constructive. And then he
shows, Gentzen's proof is that if there is a proof of contradiction, if
there is an inconsistency in formal arithmetic, then there would exist a
sequence of these ordinals which is decreasing at each step but never
terminates.  So infinite decreasing sequence of these ordinals.  And then
he, [pause] and then there is a certain “argument” (I would put it
quote-unquote), which, [pause] then he says that that's unlikely, I mean
or rather it's something like he says it's self-evident that that cannot
happen.  So this self-evidence is extremely suspicious because, in a
complete agreement with Goedel's theorem, one can show that it's
impossible to prove using the usual induction and usual enumeration
techniques that any such decreasing sequence terminates.  So it's
impossible to prove using the usual reasoning means that it terminates.
The only reason to say that it terminates is to declare that it's
self-evident.  That again is not very convincing.  So basically what it
means is that if you find inconsistency in the first order arithmetic, it
will mean that there will be this nonterminating sequence of ordinals less
than \epsilon_0, so what? That's an interesting conclusion but it's not
earth-shattering in any way.>>


He seems to be saying that there are literally no arguments that
\epsilon_0 is well-ordered.  His rhetorical question "so what?" has an
easy rejoinder from anyone familiar with ordinals.  Thus his lecture does
not give a fair portrayal of the mathematical context. I am puzzled as to
why he would do this.


Best,
Monroe