I have no idea why I wrote ACA0. I was totally wrong (ACA0 is enough for Dedekind-completeness...). But the ratio test is actually subtly difficult. > But you

I have no idea why I wrote ACA0. I was totally wrong (ACA0 is enough for Dedekind-completeness...). But the ratio test is actually subtly difficult. > But you could at least prove the validity of the ratio test for any computably enumerable sequence of computable real numbers, or such things. This still actually isn't quite true, the emphasis on "computable" being essential here. In particular the ratio test is (unless I've yet again made a catastrophic mistake) not provable in RCA0. The tricky problem with your proof sketch is the word "eventually." In general you can't find the N that validates your usage of the word "eventually" in a computable fashion. This is fundamentally different than superficially similar tests such as the alternating series test because those don't lean on "eventually" in the same way. So the ratio test is actually still uniquely difficult for (computable) finitism.