Interactive Learning Based Realizability and 1-Backtracking Games

Federico Aschieri

We prove that interactive learning based classical realizability (introduced by Aschieri and Berardi for first order arithmetic) is sound with respect to Coquand game semantics. In particular, any realizer of an implication-and-negation-free arithmetical formula embodies a winning recursive strategy for the 1-Backtracking version of Tarski games. We also give examples of realizer and winning strategy extraction for some classical proofs. We also sketch some ongoing work about how to extend our notion of realizability in order to obtain completeness with respect to Coquand semantics, when it is restricted to 1-Backtracking games.

In Steffen van Bakel, Stefano Berardi and Ulrich Berger: Proceedings Third International Workshop on Classical Logic and Computation (CL&C 2010), Brno, Czech Republic, 21-22 August 2010, Electronic Proceedings in Theoretical Computer Science 47, pp. 6–20.
Published: 27th January 2011.

ArXived at: http://dx.doi.org/10.4204/EPTCS.47.3 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org