In this talk, we will investigate the lengths of proofs in the usual Gentzen calculus for the substructural logic FL_e. We will present a sequence of tautologies of the system and show any short proof for them implies a short proof for Hrubes' formulas for intuitionistic logic, hence the exponential lower bound follows. We will then conclude that this lower bound also applies to any proof system for a logic between FL_e and IPC.
Logic seminar
usually takes place each Monday at 14:00 in IM, rear building, ground floorChair: Pavel Pudlak, Neil Thapen
More information on the old seminar web page. The programme is announced via the mailing list.
An exponential lower bound for lengths of proofs in substructural logics
Raheleh Jalali Keshavarz
Institute of Mathematics
Monday, 23. September 2019 - 13:30 to 15:00
in IM, rear building, ground floor