Skip to main content
SpringerLink
Log in

Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics

  • Conference paper
Book cover Typed Lambda Calculi and Applications (TLCA 2013)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 7941))

Included in the following conference series:

  • 644 Accesses

Abstract

This paper introduces a game semantics for Arithmetic with various sub-classical logics that have implication as a primitive connective. This semantics clarifies the infinitary sequent calculus that the authors proposed for intuitionistic arithmetic with Excluded Middle for Sigma-0-1-formulas, a formal system motivated by proof mining and by the study of monotonic learning, for which no game semantics is known. This paper proposes games with Sequential Backtracking, and proves that they provide a sound and complete semantics for the logical system and other various subclassical logics. In order for that, this paper also defines a one-sided version of the logical system, whose proofs have a tree isomorphism with respect to the winning strategies of the game semantics.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 72.00
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Akama, Y., Berardi, S., Hayashi, S., Kohlenbach, U.: An Arithmetical Hierarchy of the Law of Excluded Middle and Related Principles. In: LICS 2004, pp. 192–201 (2004)

    Google Scholar 

  2. Aschieri, F., Berardi, S.: A Realization Semantics for EM1-Arithmetic. In: Curien, P.-L. (ed.) TLCA 2009. LNCS, vol. 5608, pp. 20–34. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  3. Aschieri, F.: Learning, Realizability and Games in Classical Arithmetic. Ph. D. thesis, Torino (2011)

    Google Scholar 

  4. Aschieri, F.: Learning Based Realizability for HA + EM1 and 1-Backtracking Games: Soundness and Completeness. APAL Special Issue for CL&C 2010 (2010)

    Google Scholar 

  5. Berardi, S., De’Liguoro, U.: Interactive Realizers: A New Approach to Program Extraction. ACM Trans. Comput. Log. 13(2), 11 (2012)

    Article  MathSciNet  Google Scholar 

  6. Berardi, S., Coquand, T., Hayashi, S.: Games with 1-backtracking. Ann. Pure Appl. Logic 161(10), 1254–1269 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  7. Berardi, S., Tatsuta, M.: Positive Arithmetic Without Exchange Is a Subclassical Logic. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol. 4807, pp. 271–285. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  8. Berardi, S., De’Liguoro, U.: Toward the interpretation of non-constructive reasoning as non-monotonic learning. IC 207(1), 63–81 (2009)

    MathSciNet  MATH  Google Scholar 

  9. Berardi, S., Yamagata, Y.: A Sequent Calculus for Limit ComputableMathematics. APAL 153(1-3), 111–126 (2008)

    MathSciNet  MATH  Google Scholar 

  10. Berardi, S.: Semantics for Intuitionistic Arithmetic Based on Tarski Games with Retractable Moves. In: Della Rocca, S.R. (ed.) TLCA 2007. LNCS, vol. 4583, pp. 23–38. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  11. Berardi, S.: Interactive Realizability. Summer School Chambéry, June 14-17 (2011), http://www.di.unito.it/~stefano/Berardi-RealizationChambery-13Giugno2011.ppt

  12. Curien, P.-L., Herbelin, H.: Abstract machines for dialogue games. CoRR abs/0706.2544 (2007)

    Google Scholar 

  13. Coquand, T.: A semantics of evidence for classical arithmetic (preliminary version). In: 2nd Workshop on Logical Frameworks, Edinburgh (1991)

    Google Scholar 

  14. Coquand, T.: A semantics of evidence for classical arithmetic. Journal of Symbolic Logic 60, 325–337 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  15. Gold, E.M.: Limiting Recursion. Journal of Symbolic Logic 30, 28–48 (1965)

    Article  MathSciNet  MATH  Google Scholar 

  16. Hyland, M., Ong, L.: On full abstraction for PCF. Information and Computation 163(2), 285–408 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  17. Hayashi, S.: Mathematics based on incremental learning, excluded middle and inductive inference. Theoretical Computer Science 350(1), 125–139 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  18. Hayashi, S., Nakata, M.: Towards Limit Computable Mathematics. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) TYPES 2000. LNCS, vol. 2277, pp. 125–144. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  19. Hayashi, S.: Can Proofs be animated by games? Fundamenta Informaticae 77(4), 331–343 (2007)

    MathSciNet  MATH  Google Scholar 

  20. Herbelin, H.: Sequents qu’on calcule: de l’interpretation du calcul des sequents. Ph. D. thesis, University of Paris VII (1995)

    Google Scholar 

  21. Hodges, W.: Logic and games. In: The Stanford Encyclopedia of Philosophy, Winter (2004), http://plato.stanford.edu/archives/win2004/entries/logic-games/

  22. Felscher, W.: Lorenzen’s game semantics. In: Handbook of Philosophical Logic, vol. 5, 2nd edn., pp. 115–145. Kluwer Academic Publishers (2002)

    Google Scholar 

  23. Tatsuta, M., Berardi, S.: Non-Commutative Infinitary Peano Arithmetic. In: Proceedings of CSL 2011, pp. 538–552 (2011), Preliminary version: http://www.di.unito.it/~stefano/CSL2011-NonCommutativePeanoArithmetic.pdf

Download references

Author information

Authors and Affiliations

  1. Torino University, C.so Svizzera 185, 10149, Torino, Italy

    Stefano Berardi

  2. National Institute of Informatics, 2-1-2 Hitotsubashi, Tokyo, 101-8430, Japan

    Makoto Tatsuta

Authors
  1. Stefano Berardi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Makoto Tatsuta
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Research Institute for Mathematical Sciences, Kyoto University, Kitashirakawa-Oiwake-cho, Sakyo-ku, 606-8502, Kyoto, Kyoto, Japan

    Masahito Hasegawa

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Berardi, S., Tatsuta, M. (2013). Games with Sequential Backtracking and Complete Game Semantics for Subclassical Logics. In: Hasegawa, M. (eds) Typed Lambda Calculi and Applications. TLCA 2013. Lecture Notes in Computer Science, vol 7941. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38946-7_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-38946-7_7

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-38945-0

  • Online ISBN: 978-3-642-38946-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation