Tourlakis G. A New Arithmetically Incomplete First-Order Extension of Gl All Theorems of Which Have Cut Free Proofs. B Sect Log. 2016;45(1):17–31. doi:10.18778/0138-0680.45.1.02