 Arithmetical transfinite recursion theory

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.