[FOM] Voevodsky corr051711,11:12AM-052511,7:53AM

[Harvey Friedman]

Vladimir Voevodsky has given me permission to post this up to date  
correspondence between us. This is the second installment, and, for  
your convenience, it is cumulative.

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.

On May 22, 2011, at 4:58 PM, Harvey Friedman wrote:

Dear Vladimir,

I think we have had a fruitful correspondence. In light of my last  
email to you, do you think that "Con(PA) is a legitimate open problem  
in mathematics"?

I don't think you would regard "the existence of an infinite bounded  
sequence of rationals with no convergent (1/n) infinite subsequence"  
is a legitimate open problem in mathematics.

Harvey

On May 22, 2011, at 5:18PM, Vladimir Voevodsky wrote:

Harvey

I need to look at the reference which you gave me. It might take a few  
days.

Vladimir.

On May 22, 2011, at 5:30 PM, Harvey Friedman wrote:

The following might be useful for you.

There is my system RCA_0 spelled out in that book. This system is much  
weaker, in many senses, than PA, although it has variables over sets  
of integers.

There is my system ACA_0, also spelled out in that book. PA is  
interpretable in ACA_0. The interpretation is very direct. ACA_0 is  
finitely axiomatized.

In the book there is a proof of the logical equivalence of

RCA_0 + "infinite bounded sequences of rationals with no convergent (1/ 
n) infinite subsequences"

On May 22, 2011, at 6:28PM, Vladimir Voevodsky wrote:

What is a 1/n convergent sequence?

Vladimir.

On May 22, 2011, at 10:35 PM, Harvey Friedman wrote:
For all i,j >= n, |q_i - q_j| < 1/n.

Harvey

On May 23, 2011, at 7:15AM, Vladimir Voevodsky wrote:

Is this question related to the compactness of the unit interval in R ?

Vladimir.

On May 23, 2011, at 8:19AM, Harvey Friedman wrote:

No. There are two differences.

1. I went out of my way to avoid bringing in real numbers, for a  
number of reasons.
2. Also, the compactness of the unit interval in R is logically  
substantially weaker, and will not suffice to interpret PA.

Harvey

On May 24, 2011, at 9:28PM, Harvey Friedman wrote:

Your last email gave me the impression that our correspondence about  
Con(PA) was going to continue.

If this is the case, then I will wait patiently for your response.

If you view this round of correspondence as over, please let me know,  
as I will update the FOM email list with the complete correspondence.

It would of course be useful if you would reassess or restate your  
position that "the consistency of PA is a legitimate open problem in  
mathematics" in light of our correspondence.

Harvey

On May 25, 2011, at 7:41AM, Vladimir Voevodsky wrote:

Dear Harvey,

so far I do not plan to reassess anything in my position. I would also  
like to continue our correspondence but after some time . At the  
moment it has reached the discussion of areas which are not well known  
to me and being very actively working on other things I can not catch  
up quickly.

May be I should also state that in my opinion proving inconsistency of  
PA is out of reach for the current math knowledge and that actually  
spending time on trying to do it directly would probably be unwise.

One direction which might be both more promising and interesting as an  
intermediate step would be to try to prove inconsistency of ZFC with  
universes. But again I would not try to do it directly but rather  
retain the possibility of inconsistencies as a philosophical position  
and work on something more constructive. If there are inconsistencies  
they will show up sooner or later.

Very best,
Vladimir.

On May 25, 2011, at 7:46 AM, Harvey Friedman wrote:

I think maybe you can clear up your view on a point I was trying to  
make. It appears that contemplating the inconsistency of PA forces  
contemplating a refutation of

*every bounded infinite sequence of rationals contains a 1/n Cauchy  
subsequence*

and I would have thought that you were unwilling to contemplate such a  
refutation. Perhaps you are willing to contemplate such a refutation?  
I surmise that the overwhelmingly majority of mathematicians are not  
willing to contemplate such a refutation.

Can you clarify your position on this aspect of our correspondence?

Harvey

On May 25, 2011, at 7:53AM, Vladimir Voevodsky wrote:

That's precisely what I meant by areas which are not well known to me  
and which I have no intuition about. So at the moment, no , I can not  
comment on it and do not have a position in relation to this  
particular question.

I will however have a chance to consider this question again when I  
will be working on constructive formalizations of real numbers and  
their properties.

Vladimir.