Logo image
Sign in
From strategies to derivations and back An easy completeness proof for first order intuitionistic dialogical logic
Working paper   Open access

From strategies to derivations and back An easy completeness proof for first order intuitionistic dialogical logic

Davide Catta

Abstract

In this paper we give a new proof of the correspondence between the existence of a winning strategies for intuitionistic E-games and Intuistionistic validity for first order logic. The proof is obtained by a direct mapping between formal E-strategy 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
url
Find in HALView

Metrics

1 Record Views

Details

Logo image