[FOM] Convergent subsequences of sequences in [0,1]

[Andrej Bauer]

In recent discussions about consistency of Peano arithmetic (PA) it
was pointed out by Harvey Friedman that believing the consistency of
PA is the same as believing the statement

 Conv: "Every rational sequence in [0,1] has a convergent subsequence
with modulus of convergence 1/n."

The statement Conv cannot be proved constructively because it fails in
the effective topos (consider a Specker sequence). In other words, a
Russian constructivist would believe the negation of Conv.

So how does one show the equivalence of Con(PA) and Conv? The proof
must necessarily use a bit of classical logic, otherwise the effective
topos would validate the negation of Con(PA).

With kind regards,

Andrej Bauer

Faculty of mathematics and physics
University of Ljubljana
Slovenia
http://andrej.com/