From Strategies to Derivations and Back: An Easy Completeness Proof for First-Order Intuitionistic Dialogical Logic

In this paper, we give a new proof of the correspondence between the existence of a winning strategy for intuitionistic E-games and Intuistionistic validity for first-order logic. The proof is obtained by a direct mapping between formal E-strategies and derivations in a cut-free complete sequent calculus for first-order intuitionistic logic. Our approach builds on the one developed by Herbelin in his PhD dissertation and greatly simplifies the proof of correspondence given by Felscher in his classic paper.