[FOM] 461: Reflections on Vienna Meeting
pratt at cs.stanford.edu
Thu Jun 16 03:07:40 EDT 2011
On 6/14/2011 11:48 PM, Alex Simpson wrote:
> I don't read Angus here as saying that he believes the consistency of PA
> to be a "legitimate mathematical problem". For example, what Angus says
> is wholly compatible with the view, expressed by William Tait in his
> posting of 22nd May, that "the search for nontrivial consistency proofs
> is off the board" (since, roughly, any consistency proof is at least as
> doubtful as the system whose consistency it establishes). Also, given the
> tenor of the rest of his talk, I imagine that Angus would very
> much not view consistency investigations as the concern of legitimate
I'd be interested in seeing how this view is reconciled with Harvey's
point that Con(PA) is provable in WKL_0. It seems to me that Harvey's
offline correspondence with Voevodsky, as reported here on May 26 by
Harvey, was going well up until the following exchange, which appears to
have brought the correspondence to an untimely end.
VV: Is this question [about a 1/n Cauchy convergent subsequence of
rationals] related to the compactness of the unit interval in R ?
HF: 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.
The "no" response appears to have led VV to respond that the
correspondence has at the moment "reached the discussion of areas which
are not well known to me."
Surely the correct answer to VV's question would have been "yes." The
subtext of this exchange as I understood it was not directly about
logical strength but simply whether VV would accept the existence of a
1/n Cauchy convergent subsequence of rationals. Assuming he's ok with
Koenig's Lemma for binary trees, he should be ok with that existence.
since the original proof of the Heine-Borel theorem based on Koenig's
Lemma, which must be well known to VV, does not raise any obvious (to
me) concerns for the unit interval in Q. The point that its application
to Q raises arithmetic issues that do not arise when applied to R (if
that's the correct interpretation of Harvey's "no"), which may well be
unknown to VV, seems a distraction in this context.
The interesting question here would be, does VV have any problem with
Koenig's Lemma for binary trees? If so it would be instructive to
understand his objection to it. If not, what other concern could he
have about WKL_0?
More information about the FOM