A sequent calculus for limit computable mathematics

We introduce an implication-free fragment of ω-arithmetic, having Exchange rule for sequents dropped. Exchange rule for formulas is, instead, an admissible rule in . Our main result is that cut-free proofs of PA-ω without Exchange are isomorphic with recursive winning strategies of a set of games called “1-backtracking games” in [S. Berardi, Th. Coquand, S. Hayashi, Games with 1-backtracking, Games for Logic and Programming Languages, Edinburgh, April 2005]. We also show that PA-ω without Exch is a sound and complete formal system for the implication-free fragment of LCM (Limit Computable Mathematics, see [S. Hayashi, Mathematics based on Learning, Algorithmic Learning Theory, in: LNAI, vol. 2533, Springer, pp. 7–21; S. Hayashi, Can proofs be animated by games? in: P. Urzyczyn (Ed.), Seventh International Conference on Typed Lambda Calculi and Applications, in: Lecture Notes in Computer Science, vol. 3461, 2005, pp. 11–22. Invited paper]). A simple syntactical description of this fragment was still missing. No sound and complete formal system is known for LCM itself.