[FOM] 461: Reflections on Vienna Meeting

[Vaughan Pratt]

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
> mathematics.

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?

Vaughan Pratt