Sequent Calculus, Dialogues, and Cut-Elimination
Abstract
It is well-known that intuitionistic and classical provability can be characterized by the existence of winning proponent strategies in Lorenzen dialogues. In fact, one can bring the winning proponent strategies more or less into correspondence with sequent calculus proofs.
This paper elaborates on the correspondence. We study a variant of sequent calculuswith only one right rule and one left rule. The rules do not concern any particular connective. They are similar to the definition of Lorenzen dialogues laying out the interaction between proponent and opponent. In the latter setting one additionally specifies, for each connective, the attacks and corresponding defenses. Similarly, our left and right rule are parameterized by such specifications.
The main result is cut-elimination for the system without specification of the actual connectives. Cut-elimination for any combination of the usual connectives follow as a special case. We also give a very compact proof that derivations in the system are isomorphic to winning proponent strategies. We focus on classical propositional logic. The results carry over to intuitionistic logic as well as first-order logic, and the equivalence of proofs and strategies also carry over to second-order logic, in all cases with some adjustments.
Full text