Lehman College - CUNY Graduate Center
Gentzen proved a famous cut elimination theorem using constructive methods. It is also possible to prove it non-constructively, with a conceptually simpler argument, but a constructive proof is important for a number of reasons. I will present the constructive argument for cut elimination, for classical propositional logic, formulated using tableaus. This is purely expository; there is nothing new. But it is a proof that every logician, or logician-to-be, should know, and I will cover the basics using a detailed set of slides which will be made available afterward, on my web site.
Lehman College Professor Melvin Fitting received the Herbrand Award of 2012 for his groundbreaking contributions to the field of automated theorem proving, which focuses on getting computer programs to prove logical and mathematical deductions.