Arithmetical transfinite recursion theory (${\mathsf{ATR}}_0$)

Arithmetical transfinite recursion theory permits arithmetic recursive definitions along coded countable well-orders, together with the usual arithmetic comprehension background. Friedman's finite form of Kruskal's theorem is not provable in this theory.