Arithmetical transfinite recursion theory
= Arithmetical transfinite recursion theory
{title2=$\mathsf{ATR}_0$}
= ATR0
{c}
{synonym}
<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.