Goodstein's theorem without transfinite induction

Goodstein's theorem is an example of a theorem that is not provable from first order arithmetic. All proofs of the theorem seem to deploy transfinite induction and I've wondered if one could prove the theorem without transfinite induction. Some time ago I came across this old usenet post where Torkel Franzen writes

Goodstein's theorem does not necessarily require transfinite induction for its proof, but it's not provable in elementary arithmetic. It can be proved by ordinary induction on a statement involving quantification over sets...

What is the proof/statement Franzen is referring to?

-
Note, that Goodstein can be proven in second order logic. So, if the sets are defined by predicates and you allow quantification over it, you have effectively a second order system. The proof in such system might however become close to the transfinite proof. – Lucas K. Jun 24 '13 at 18:09
Interesting! Have you checked Franzen's Inexhaustibility book? Sounds like this is a concrete way to see that $ACA_0$ with $\Sigma^1_1$-induction is not conservative over $PA$. – François G. Dorais Jun 24 '13 at 18:26
I have been thinking how exactly the second order proof goes. One should prove that if the exponents follow a well ordered relation, then the newly created relation is also well ordered. Which such proof, you can then do induction on the height of the exponent tower. Because, we are quantifying over all well ordered relations, this is a second order proof. In case of meta-logic (using Constructive omega rule), the quantification is on syntactical level. – Lucas K. Jun 25 '13 at 18:39
I'm out of the office so I can't check but Google books tells me there are four matches for "Goodstein" in the book (one of which is in the index). So I think it's worth a trip to the library. – François G. Dorais Jun 28 '13 at 12:08

But the way that your prove it for each $n$ is essentially by transfinite induction up to the particular ordinal represented by replacing $2$ with $\omega$ in the complete base $2$ representation of $n$. The point is that PA is strong enough to prove that the corresponding relation is a well-order for each specific $n$ separately, but not that the full relation, corresponding to ordinal $\epsilon_0$, is a well-order. – Joel David Hamkins Jun 24 '13 at 18:02
I am saying that the proof in that system that I know is essentially the transfinite proof (but using codes for the ordinals as natural numbers). That is, to prove instance $n$ in PA, you in effect interpret $n$ as coding an ordinal, and use the fact that PA can prove that there is no infinite descending sequence of ordinals starting from that code. – Joel David Hamkins Jun 24 '13 at 21:34