When Gentzen (1935) developed his sequent calculi, rather than using sets of formulas as contexts, he used lists of formulas and added explicit structural rules of exchange, weakening, and contraction. Later, Lambek (1958) and Girard (1987) showed that (with minor modifications) sequent systems with subsets of those structural rules have the same desirable proof theoretic properties of the original system. However, Gentzen's choice of lists is somewhat arbitrary. If instead we consider binary trees (Lambek 1961), we obtain the weakest logic satisfying the deduction theorem, an arguably more canonical choice. We recapture list contexts from this system by introducing an explicit associativity structural rule. We now have four structural rules, and each of the sixteen subsets gives a cut-eliminable sequent system.
Logic and Computation Seminar
Monday, October 14, 2024 - 3:30pm
Eben Blaisdell
..
We consider the decidability of provability in these logics. The 4 with contraction and weakening collapse to IPL and are thus decidable; the rest are all distinct. The 8 without contraction are trivially decidable by bounded proof search. Kripke (1959) showed that the logic with contraction, associativity, and exchange is decidable. We get closer to finishing this story by presenting an argument for the decidability of the remaining nonassociative logics.