G. Tourlakis, “A New Arithmetically Incomplete First-Order Extension of Gl All Theorems of Which Have Cut Free Proofs”, B Sect Log, vol. 45, no. 1, pp. 17–31, Mar. 2016.