Dialogues, strategies, and intuitionistic provability (Q1061740): Difference between revisions

This paper presents an equivalent theorem proof, namely that for every winning strategy in certain Lorenzen-style dialogue games there is a proof in LJ, the Gentzen consecution calculus for intuitionistic logic, and vice versa. There is an algorithm for transforming either into the other. In addition, for propositional languages, every LJ proof can be transformed into an irreducible normal form.