Damian Szmuc

The aim of this talk is to examine the class of Gentzen-style sequent calculi where Cut is admissible but not derivable that prove all the (finite) inferences that are usually taken to characterize Classical Logic—conceived with conjunctively-read multiple premises and disjunctively-read multiple conclusions. We’ll do this starting from two different calculi, both counting with Identity and the Weakening rules in unrestricted form. First, we’ll start with the usual introduction rules and consider what expansions thereof are appropriate. Second, we’ll start with the usual elimination or inverted rules and consider what expansions thereof are appropriate. Expansions, in each case, may or may not consist of additional standard or non-standard introduction or elimination rules, as well as of restricted forms of Cut.

---