Interactive Learning Based Realizability and 1-Backtracking Games

TL;DR

This paper establishes a connection between interactive learning based realizability and Coquand game semantics, showing that realizers correspond to winning strategies in 1-Backtracking Tarski games for certain formulas.

Contribution

It proves soundness of interactive learning based realizability with respect to Coquand game semantics and demonstrates how realizers can be extracted as winning strategies.

Findings

Realizers embody winning recursive strategies for 1-Backtracking Tarski games.

Examples of realizer and strategy extraction for classical proofs.

Discussion on extending realizability to achieve completeness with Coquand semantics.

Abstract

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.