[FOM] Convergent subsequences of sequences in [0,1]
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,
Faculty of mathematics and physics
University of Ljubljana
More information about the FOM