[FOM] Voevodsky corr051711,11:12AM-052511,7:53AM
Harvey Friedman
friedman at math.ohio-state.edu
Wed May 25 09:20:45 EDT 2011
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.
More information about the FOM
mailing list