[FOM] Voevodsky corr051711,11:12AM-052211,11:05AM
Harvey Friedman
friedman at math.ohio-state.edu
Sun May 22 11:54:52 EDT 2011
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
More information about the FOM
mailing list