[FOM] Cauchy subsequences of rationals and Con(PA)

[David Roberts]

Dear Harvey,

you wrote (2 October):

--
>As I indicated before on the FOM, there is a proof that any given finite fragment of PA is consistent, using
>"every infinite sequence of rationals in [0,1] has an infinite Cauchy 1/n subsequence".
--

Let the statement "every infinite sequence of rationals in [0,1] has
an infinite Cauchy 1/n subsequence" be denoted CSR. I have seen you
make this similar statements involving CSR several times, for example
on June 14 this year:

--
>Let me add that modulo some interesting strict reverse mathematics,
>the statement

>"every infinite sequence of rationals from [0,1] has an infinite 1/n
>style Cauchy subsequence"

>outright implies (and is used by a large number of mathematicians
>Angus has no reservations about)

>"PA restricted to 100 quantifier inductions is consistent".
--

(and go on to say that the 100 is really an arbitrary finite number)

And in your posting on May 25 this year of your Voevodsky correspondence:

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

referring to an earlier email from the corespondence (in the same post)
where you wrote

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

I like the look of this result. However my question is: what is the
exact status of the result that CSR => Con(PA)? Is there a precise
statement of this anywhere? I have followed most of what you have said
in the two recent episodes about Con(PA) on fom and not seen it.

Also, can we replace KT by CSR in the immediately preceeding quote,
keep the statements A_1 ... A_15 and arrive at Con(PA)? If so, what
are A_1 ... A_15? (I gather or presume these are detailed in SImpson's
book, to which I do not have access. If so, please humour me.)

Is the 'interesting strict reverse mathematics' involved in CSR =>
Con(PA) at public release stage? Or still in development?

My list of questions is already too long; I apologise, but this has
been a nagging itch for me.

(sort of PS: Andrej Bauer said on MathOverflow--answering a question
of mine--that there is no constructive proof of CSR, because in the
effective topos it is false. But that is perhaps a discussion for
another time.)

Thanks,

David Roberts
--
Visiting Research Fellow
School of Mathematical Sciences
University of Adelaide