 Theorem 3.9 (Kleene 1943): For all \(k\), there exists a \(\Sigma^0_1\)-formula \(\sigma_{k,1}(x,\vec{y})\) such that for all \(\Sigma^0_1\)-formulas with \(k\)-free variables \(\varphi^k_e(\vec{y})\), the following biconditional 