Arithmetical transfinite recursion theory (source code)

= 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.