[FOM] Voevodsky Correspondence

[Harvey Friedman]

Recall that I started my correspondence with Vladimir Voevodsky with  
this:

> Dear Professor Voevodsky,
>
> I have become aware of your online videos at http://video.ias.edu/voevodsky-80th 
>  and http://video.ias.edu/univalent/voevodsky. I was particularly  
> struck by your discussion of the "possible inconsistency of Peano  
> Arithmetic". This has created a lot of attention on the FOM email  
> list. As a subscriber to that list, I would very much like you to  
> send us an account of how you view the consistency of Peano  
> Arithmetic. In particular, how you view the usual mathematical proof  
> that Peano Arithmetic is consistent, and to what extent and in what  
> sense is "the consistency of Peano Arithmetic" a genuine open  
> problem in mathematics. It would also be of interest to hear your  
> conception of what foundations of mathematics is, or should be, or  
> could be, as it appears to be very different from traditional  
> conceptions of the foundations of mathematics.
>
> Respectfully yours,
>
> Harvey M. Friedman

Recall that I received the following reply:

> From: Vladimir Voevodsky <vladimir at ias.edu>
> Date: May 18, 2011 4:44:13 PM EDT
> To: Harvey Friedman <friedman at math.ohio-state.edu>
> Cc: Vladimir Aleksandrovich Voevodsky <vladimir at ias.edu>
> Subject: Re: invitation to comment
>
> Dear Harvey,
>
> such a comment will take some time to write ...
>
> To put it very shortly I think that in-consistency of Peano  
> arithmetic as well as in-consistency of ZFC are open and very  
> interesting problems in mathematics. Consistency on the other hand  
> is not an interesting problem since it has been shown by Goedel to  
> be impossible to proof.
>
> Vladimir.

I also wrote the following letter to Angus:

> Dear Angus MacIntyre,
>
> Greetings!
>
> I have put up a detailed critique surrounding our presentations at  
> the recent meeting in Vienna. See http://www.cs.nyu.edu/pipermail/fom/2011-May/015391.html 
>  . This has attracted a lot of attention on the FOM email list. As a  
> subscriber to that list, I would very much like you to send us your  
> views on the relevant issues. In particular, your view as to the  
> extend to which the consistency of Peano Arithmetic is a genuine  
> open problem in mathematics - as you indicated in your talk. You may  
> also recall that I challenged you to return to Vienna with me for a  
> formal debate with strict rules of engagement. As you know, your  
> views are at considerable odds in many respects with the traditional  
> f.o.m. point of view. I am asking you to engage in a substantive  
> debate on the FOM email list, which is carefully moderated by a  
> dedicated moderator and FOM editorial board - in order that the  
> relevant ideas being fully tested in depth, in an open and fair  
> intellectual form.
>
> Respectfully yours,
>
> Harvey M. Friedman

Unfortunately, I have yet to get a response from Angus. I will resend  
the message shortly, mentioning that Vladimir has responded.

I now continue my correspondence with Vladimir with the following reply.

Dear Vladimir,

Thanks for your quick response of May 18 to my letter of May 17.

How would you assess the various proofs of the consistency of PA that  
we now have, for your purposes? There are quite a number of them,  
using various hypotheses.

One relatively new kind of proof of Con(PA) is the proof that uses the  
following well known and beautiful theorem of J.B. Kruskal, which I  
call KT (Kruskal's Theorem):

*in every infinite sequence of finite trees, some tree is  
homeomorphically embeddable into a later tree*

We have a lot of control over the implication "KT implies Con(PA)".  
This implication can be proved using extremely innocent principles -  
in particular, not using anything like the full power of PA.

In fact, using ideas from my Strict Reverse Mathematics, I believe  
that this implication can be proved without using any logical  
principles whatsoever, other than the normal everyday logic of not,  
and, or, if then, iff, forall, therexists. More precisely, there are  
about 15 well known mathematical theorems, KT being the only  
nontrivial one, such that the implication

(A_1 and ... and A_15 and KT) implies Con(PA)

can be proved just using the normal everyday logic of not, and, or, if  
then, iff, forall, therexists, even without the law of the excluded  
middle - specifically, in so called constructive logic.

Harvey

Given the quick response to the first letter, I am expecting a  
response to this second letter.

Harvey Friedman