[FOM] Voevodsky corr051711,11:12AM-052211,11:05AM

[Harvey Friedman]

Vladimir Voevodsky has given me permission to post this up to date  
correspondence between us.

On May 17, 2011, at 2:45 PM, Harvey Friedman wrote:

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
Ohio State University
Distinguished University Professor
Mathematics, Philosophy, Computer Science

On May 18, 2011, at 4:44 PM, Vladimir Voevodsky wrote:

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.

On May 20, 2011 11:48:05 PM EDT, Harvey Friedman wrote:

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

On May 21, 2011 12:07PM Vladimir Voevodsy wrote:

Well, that would contradict Goedel's result. I do not know Krushkal's  
theorem but I would suspect that it uses some sort of transfinite  
induction explicitly or in a hidden way.

Vladimir.

On May 21, 2011 12:31:03PM, Harvey Friedman wrote:

The standard proof of Kruskal's theorem uses a specific form of  
comprehension axiom for building sets of integers.

When you say "Con(PA) is impossible to prove", I thought you meant  
"impossible to prove using accepted mathematical principles". Perhaps  
you just mean that Con(PA) is impossible to prove within PA - just that?

Harvey

On May 21, 2011, at 2:27 PM, Vladimir Voevodsky wrote:

Pretty much just that. Because the "accepted mathematical principles"  
are themselves no more reliable in terms of consistency than PA. In  
fact, one would obviously expect that it will be easier to prove the  
inconsistency of principles which can be used to prove consistency of  
PA than inconsistency of PA itself.

Vladimir.

On May 21, 2011, at 3:26 PM, Vladimir Voevodsky wrote:

There is Gentzen's "proof" of consistency of PA. I looked through it  
in the book by Takeuti who describes all the related definitions in  
finitary terms. What the proof requires however is that certain  
algorithm ("normalization" of the ordinals < epsilon ) always  
terminates. This follows from the part of set theory which guarantees  
the existence of epsilon but does not follow from anything else.

It is very typical, that the consistency issues are related to the  
termination for different algorithms and in this case it is a very  
explicit combinatorial algorithm but there is no mathematical proof  
that it terminates.

Vladimir.

On May 21, 2011 4:34:11PM, Harvey Friedman wrote:

Apparently, you think it worthwhile to spend some of your time to  
prove the inconsistency of PA. Un my opinion, that result would be the  
greatest result of all time in mathematics by orders of magnitude. And  
that doesn't touch on how it would compare with results in science and  
general human intellectual activity.

Do you have some reason for working on this other than working on the  
opposite is precluded by Goedel? Actually, working on giving a  
consistency proof of PA within PA is actually exactly the same  
problem, by Goedel.

Harvey

On May 22, 2011 10:30AM, Vladimir Voevodsky wrote:

I do not really work on it. At least not actively. I am working full  
time on new foundations and the related type theoretic formalization  
which should finally make it possible for the working mathematicians  
to use proof development software.

The issue of inconsistencies was just somethings I had to come to  
grips with and it make for a good lecture topic at that time.

Vladimir.

On May 21, 2011 4:36:33 PM, Harvey Friedman wrote:

There is a mathematical proof that it terminates. I assume that this  
proof uses principles that you do not accept as legitimate for this  
purpose? E.g., the termination can be proved in RCA_0 + infinite  
Ramsey theorem.

Harvey

May 22, 2011 10:32AM, Vladimir Voevodsky wrote:

You are right, I was sloppy in my formulations.
V.

On May 21, 2011 4:46 PM, Harvey Friedman wrote:

I mentioned before proving Con(PA) from KT = Kruskal's Theorem, and  
also from IRT = infinite Ramsey's Theorem.

One can also use "every bounded sequence of rationals contains a {1/n}  
convergent subsequence".

See my previous discussion of such implication proofs.

In particular, any proof of not Con(PA) is going to refute "every  
bounded sequence of rationsls contains a {1/n} convergent subsequence.

Harvey

On May 22, 2011 10:26AM, Vladimir Voevodsky wrote:

Could you give a reference on this result about sub-sequences ?

Thanks!
Vladimir.

On May 22, 2011, 11:05AM, Harvey Friedman wrote:

Regarding the sentence A = "every bounded sequence of rationals  
contains a (1/n) convergent subsequence". Actually I overstated my  
claim. What one has is an interpretation of PA in a weak set of  
statements plus A. So any inconsistency in PA is then transferred to a  
refutation of A (assuming the weak set of statements is  
unimpeachable). The typical reference for this is III.2 of Subsystems  
of Second Order Arithmetic, Steve Simpson.

Typically this is done over the base theory RCA_0 of RM = Reverse  
Mathematics. RCA_0 is much much weaker than PA in many senses. In SRM  
= strict reverse mathematics, we can avoid a logically oriented theory  
such as RCA_0.

I have to prepare a talk for a workshop on Reverse Mathematics, and  
this is just the sort of thing that I will prepare from the SRM point  
of view.

Harvey