A Direct Proof of Schwichtenberg's Bar Recursion Closure Theorem

Paulo Oliva, Silvia Steila

In 1979 Schwichtenberg showed that the System $\text{T}$ definable functionals are closed under a rule-like version Spector's bar recursion of lowest type levels $0$ and $1$. More…