Adventures in Natural Deduction

Shawn Standefer (University of Melbourne)

Shawn Standefer (Melbourne) will present "Adventures in Natural Deduction". The talk will start at 11 in G14 Old Quad.

Abstract: Two kinds of natural deduction proof system are common: tree-style and Fitch. Tree-style natural deduction has been the focus of much of the proof-theoretic investigation of natural deduction systems. Fitch systems do not receive as much attention, although Brady (2006) provides an exception. In this talk, I will present a translation between Fitch proofs and tree-style proofs. This translation will shed some light on how structural rules are incorporated into the systems for intuitionistic and classical logic. I will extend this translation to classical S4. Time permitting, I will saying something about normalization. I close with a few words about future directions of research.