A sequent calculus for Limit Computable Mathematics

Annals of Pure and Applied Logic 153 (1-3):111-126 (2008)
  Copy   BIBTEX


We introduce an implication-free fragment image of ω-arithmetic, having Exchange rule for sequents dropped. Exchange rule for formulas is, instead, an admissible rule in image. Our main result is that cut-free proofs of image 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 image is a sound and complete formal system for the implication-free fragment of LCM , 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



    Upload a copy of this work     Papers currently archived: 77,916

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Cuts, Gluts and Gaps.Vincent Degauquier - 2012 - Logique Et Analyse 55 (218):229-240.
Uncomputably Noisy Ergodic Limits.Jeremy Avigad - 2012 - Notre Dame Journal of Formal Logic 53 (3):347-350.
Varieties of linear calculi.Sara Negri - 2002 - Journal of Philosophical Logic 31 (6):569-590.
Translations from natural deduction to sequent calculus.Jan von Plato - 2003 - Mathematical Logic Quarterly 49 (5):435.
A proof-search procedure for intuitionistic propositional logic.R. Alonderis - 2013 - Archive for Mathematical Logic 52 (7-8):759-778.


Added to PP

4 (#1,249,634)

6 months
1 (#485,121)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

Stefano Berardi
Università degli Studi di Torino

Citations of this work

Games with 1-backtracking.Stefano Berardi, Thierry Coquand & Susumu Hayashi - 2010 - Annals of Pure and Applied Logic 161 (10):1254-1269.
Inside the Muchnik degrees I: Discontinuity, learnability and constructivism.K. Higuchi & T. Kihara - 2014 - Annals of Pure and Applied Logic 165 (5):1058-1114.

Add more citations

References found in this work

Logic and games.Wilfrid Hodges - 2008 - Stanford Encyclopedia of Philosophy.
A semantics of evidence for classical arithmetic.Thierry Coquand - 1995 - Journal of Symbolic Logic 60 (1):325-337.
Games with 1-backtracking.Stefano Berardi, Thierry Coquand & Susumu Hayashi - 2010 - Annals of Pure and Applied Logic 161 (10):1254-1269.

Add more references