Theorem statable in base system but not provable in base system?

Question

On the wikipedia page for proof theory, under the section of reverse mathematics, it is stated that:

For each theorem that can be stated in the base system but is not provable in the base system, the goal is to determine the particular axiom system (stronger than the base system) that is necessary to prove that theorem.

As far as I understand, by a “base system” they mean a set of axioms.

I’m confused by this statement, because it seems to me that you don’t need any axioms to state a theorem, you just need a set of symbols.

What does it mean for a theorem to be “statable but not provable in a base system”?

More general bonus question: I know this question is more specifically about reverse mathematics, but can you suggest a good textbook on proof theory?

Answer 1

Wikipedia is of variable quality when it comes to maths! I'd read

... can be stated in the base system but is not provable in the base system

as slightly careless shorthand for

... can be stated in the language of the base system but is not provable in the base system.

or if you want to be more explicit still

... can be stated in the language of the base system but is not provable from the axioms of the base system using its available rules of inference.

For annotated recommendations of some books on proof theory at various levels, see §6.1 of this Study Guide.