A sequent calculus for limit computable mathematics Export

@article{citeulike:2894338, abstract = {We introduce an implication-free fragment of [omega]-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 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 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.}, author = {Berardi, Stefano and Yamagata, Yoriyuki}, booktitle = {Special Issue: Classical Logic and Computation (2006)}, citeulike-article-id = {2894338}, citeulike-linkout-0 = {http://dx.doi.org/10.1016/j.apal.2008.01.006}, citeulike-linkout-1 = {http://www.sciencedirect.com/science/article/B6TYB-4S08YD7-1/1/2fefe0a470319f164822d54390636de0}, doi = {10.1016/j.apal.2008.01.006}, journal = {Annals of Pure and Applied Logic}, keywords = {mypaper}, month = {April}, number = {1-3}, pages = {111--126}, posted-at = {2008-07-09 02:32:30}, priority = {2}, title = {A sequent calculus for limit computable mathematics}, url = {http://dx.doi.org/10.1016/j.apal.2008.01.006}, volume = {153}, year = {2008} }

TY - JOUR ID - citeulike:2894338 L3 - citeulike-article-id:2894338 N2 - We introduce an implication-free fragment of [omega]-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 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 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. IS - 1-3 JF - Annals of Pure and Applied Logic EP - 126 TI - A sequent calculus for limit computable mathematics VL - 153 T2 - Special Issue: Classical Logic and Computation (2006) SP - 111 KW - mypaper AU - Berardi, Stefano AU - Yamagata, Yoriyuki PY - 2008/04// UR - http://dx.doi.org/10.1016/j.apal.2008.01.006 ER -