Connecting Sequent Calculi with Lorenzen-Style Dialogue Games

Lorenzen has introduced his dialogical approach to the foundations of logic in the late 1950s to justify intuitionistic logic with respect to first principles about constructive reasoning. In the decades that have passed since, Lorenzen-style dialogue games turned out to be an inspiration for a more pluralistic approach to logical reasoning that covers a wide array of nonclassical logics. In particular, the close connection between (single-sided) sequent calculi and dialogue games is an invitation to look at substructural logics from a dialogical point of view. Focusing on intuitionistic linear logic, we illustrate that intuitions about resource-conscious reasoning are well served by translating sequent calculi into Lorenzen-style dialogue games. We suggest that these dialogue games may be understood as games of information extraction, where a sequent corresponds to the claim that a certain information package can be systematically extracted from a given bundle of such packages of logically structured information. As we will indicate, this opens the field for exploring new logical connectives arising by consideration of further forms of storing and structuring information.

Dialogues for proof search

Dialogue games are a two-player semantics for a variety of logics, including intuitionistic and classical logic. Dialogues can be viewed as a kind of analytic calculus not unlike tableaux. Can dialogue games be an effective foundation for proof search in intuitionistic logic (both first-order and propositional)? We announce Kuno, an automated theorem prover for intuitionistic first-order logic based on dialogue games.

Playing Lorenzen Dialogue Games on the Web

We announce an interactive website for exploring logic with the help of Lorenzen dialogue games. The site allows one to play concrete dialogue games and compute winning plays and winning strategies from initial segments of such games. A variety of dialogue rule sets are available, allowing one to explore different logics through a uniform framework. We have also implemented several formula translations, so that one can explore how games vary as one changes the initial formula of a dialogue game, and we consider some heuristics for computing winning plays and winning strategies.