[FOM] convergent subsequences

[Fernando Jorge I Ferreira]

Let  Conv be

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

The following is true: Conv is equivalent to ACA_0 over RCA_0. The reason stems from the existence of 
Specker sequences: from Conv one can show the existence of Pi^0_1 sets and, by iterating and 
relativizing this procedure, one gets full arithmetical comprehension (i.e., one gets ACA_0).
Since, finitistically, one has Con(PA) <--> Con(ACA_0), one concludes (finitistically) that Con(PA) <--> 
Con(RCA_0 + Conv). 
The effective topos validates the negation of Conv. It does not follow that it also validates the negation 
of Con(PA).
Best wishes,

Fernando Ferreira
Departamento de Matemática
Faculdade de Ciências
Universidade de Lisboa
Campo Grande, Edifício C6, Gabinete 6.2.8
P-1749-016 Lisboa
Portugal

http://www.ciul.ul.pt/~ferferr/