@Neel: I think I'd call all this type theory, which is logic.

willing to iterate along all computable well-orderings ... imply all true Pi-0-1 statements - IIRC, this isn't true: you need more than the computable WOs to get such strong soundness results. I think we need to track down a reference to sort out these battling indistinct recollections!

Talk of first-order logic and "normal circumstances" makes me unsure as to exactly what you want here. The set of interpretations open to the infix symbol "^" are the same as those open to "+" - there must be some fixing of interpretations to be able to make your language describe exponentiation: what do you have in mind?

@Joel: Oh yes, I had misremembered the CNFT. To put things in lambda-calculus terms, the CNFT gives a head normal form, not the recursive full normal form. @Asaf, sorry.

@Joel: More so, this "normal form" for these ordinals isn't unique. The CNFT only applies to ordinals less than epsilon-0.

Note that Friedman uses not simple consistency but the rather stronger notion of Sigma-1 soundness.

Obligatory link: xkcd.com/221

@Andreas: L&S use finite products and coproducts, as fits with their general discipline of specifying categorical constructions using only equations.

Right, but there's a constraint on base systems, namely that you need to be able to do reverse mathematics over them. The quote of Friedman I cited in my answer gives a case for saying ERCA-0 might be the weakest reasonable base system: not a strong case, but a "best we can do now" sort of case. I fixed my answer to make this a little clearer.