Sequent calculi and intutionistic logic
Tarmo Uustalu
Reykjavik University and Tallinn University of Technology
Abstract:
Designing sequent calculi for proof search, or even just proof analysis, is not as straightforward or noncontroversial for intutionistic propositional logic as it is for classical propositional logic. The main tensions are: should sequents be single-succedent or multiple-succedent and how to achieve termination of proof search. The troubles come, one may argue, from the structural rules; therefore it is instructive to think of what is happening in (multiplicative-additive) intuitionistic linear logic.
There is no new research in this talk. It is a review and explanation of some classic material, meant as a preparation for Elaine Pimentel's course at Viinistu.