[FOM] Ineffective proofs and weak systems

[Timothy Y. Chow]

There's a simple point about ineffective proofs that I'm confused about.
Consider the following famous theorems of number theory.

  Mordell's finite basis theorem: The group G of rational points on an
  elliptic curve defined over Q is finitely generated.

  Roth's theorem: For every algebraic alpha and every k > 2, there exist
  only finitely many rationals p/q satisfying |alpha - p/q| < 1/q^k.

The proofs are notorious for being ineffective.  The proof of the finite
basis theorem yields no algorithm for computing the rank of (the free part
of) G.  Now, what I'm confused about is, does this present any obstacle
to formalizing the proof in, say, RCA_0?  Superficially, I don't see an
immediate obstacle.  The usual proof of the finite basis theorem proceeds
by showing that G/2G is finite.  This in turn is shown by defining a
homomorphism whose kernel is 2G, and then showing that the image is finite
(by appealing to the finiteness of the ideal class group and the
multiplicative group of units of a ring of integers of a number field).
The thing is that it is easy to get an effective upper bound on the size
of G/2G and hence on the rank of G, even though there isn't any known way
of computing the rank exactly.  So offhand I don't see why this couldn't
be formalized in RCA_0.  On the other hand, isn't RCA_0 supposed to
capture "recursive mathematics" in some sense?

As for Roth's theorem, I haven't studied the proof, but I have the
impression that at a high level it proceeds by assuming there are
infinitely many solutions and then deriving a contradiction.  In
any case it is clear that for any *given* p/q, one can check the
inequality |alpha - p/q| < 1/q^k effectively, and the problem is
that there is no effective bound on the size of p/q.  Intuitively,
the ineffectivity is of a slightly different kind from that of the
finite basis theorem.  Does this make any difference as far as
formalizing in weak systems goes?

Perhaps I'm confusing "recursive mathematics" (as represented by RCA_0)
with intuitionism?

Tim