Maybe it is the advancing years, but occasionally there are those moments of panic. I think “Surely it must be the case that P“, guess I can see how to prove it, check out an obvious source or two, google around, and then am perhaps a bit surprised not to come across a straight proof of P. And sometimes my nerve fails: just occasionally I’ve asked on FOM whether indeed P. I’ve invariably got helpful replies. A couple of days ago, I was asking — in effect — how far up the Friedman/Simpson hierarchy of second-order arithmetics we have to go before we can prove Goodstein’s Theorem (something not mentioned in Simpson’s wonderful book). Before the day was out, I got a couple of really useful private responses, and there are now two brief but equally helpful replies on the list from Dmytro Taranovsky and Ali Enayat. What a fantastic resource this is: I’m not sure how my current book project would be going if it weren’t for FOM and its archives, and I’m immensely grateful.
Oh, and the answer to my question is that ATR_0 is enough. Which I should have got from Sec. V.6 of Simpson (which tells us that ATR_0 is good at handling countable well-orderings).