Lower order axioms

[Anton Freund]

> What natural axiom systems *for arithmetic* extend the Peano axioms?

I think this is a very interesting question, and I would also like to know
more about it. A classical answer seems to be: if a theory T has
proof-theoretic ordinal A, then the statement "all arithmetical
consequences of T are true" is equivalent to transfinite induction along A
for arithmetical induction formulas.

A related example (based on work of Harvey Friedman) arises from Kruskal's
tree theorem. One formulation of the latter asserts that any property of
finite trees has a finite basis. If we restrict to arithmetical
properties, this is naturally expressed by an axiom scheme in the language
of Peano arithmetic. Details can be found in the following paper:

A. Freund, A mathematical commitment without computational strength,
The Review of Symbolic Logic (to appear), https://arxiv.org/abs/2004.06915

An even stronger axiom scheme arises when we replace Kruskal's theorem by
the graph minor theorem.

Kruskal's theorem is equivalent to the well-foundedness of a certain
ordinal and hence to a principle of transfinite induction (references can
be found in the paper above). In my opinion, the equivalent statements
have different advantages: Kruskal's theorem is very natural from the
viewpoint of mathematical practice, but one would probably view it as a
theorem that requires proof, not as an axiom. Transfinite induction can
probably count as a natural axiom, but it is not quite as close to
mathematical practice. I would be very interested in further examples as
well.

Best,
Anton