12 January 2021, The Utrecht Logic in Progress Series (TULIPS), Raheleh Jalali

Abstract: Given a proof system, how can we specify the "hardness" of its theorems? One way to tackle this problem is taking the lengths of proofs as the corresponding hardness measure. Following this route, we call a theorem hard when even its shortest proof in the system is "long" in a certain formal sense. Finding hard theorems in proof systems for classical logic has been an open problem for a long time. However, in recent years as a significant progress, many super-intuitionistic and modal logics have been shown to have hard theorems.

In this talk, we will extend the aforementioned result to also cover a variety of weaker logics in the substructural realm. We show that there are theorems in the usual calculi for substructural logics that are even hard for the intuitionistic systems. More precisely, we provide a sequence of substructural tautologies {A_n}_{n=1}^{\infty} in a way that even their shortest intuitionistic proofs are exponentially long in the lengths of A_n.