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

Andrej Bauer andrej.bauer at andrej.com
Fri Jul 1 18:48:31 EDT 2011

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

More information about the FOM mailing list