SEQUENT CALCULUS, DIALOGUES, AND CUT-ELIMINATION
Morten Heine Sørensen, Paweł Urzyczyn · 2007
It is well-known that intuitionistic and classical provability can be character- ized 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 calculus with only one right rule and one left rule. The rules do not concern any particular con- nective. 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 con- nectives. 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.