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.

A sequent calculus for limit computable mathematics

BERARDI, Stefano;
2008-01-01

Abstract

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.
2008
153
111
126
http://www.journals.elsevier.com/annals-of-pure-and-applied-logic/
substructural logic; classical logic; intuitionistic logic
Stefano Berardi; Yoriyuki Yamagata
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2318/37037
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 6
  • ???jsp.display-item.citation.isi??? 4
social impact