Regular rates (register after April 15):
Rutgers affiliate, not volunteering: $75 Academic: $200 Non-academic/industry: $400
Rutgers students volunteering: free!
Natural Deduction for The Working Logician
Since the time of the founding fathers (Gentzen and Jaskowski in the 30s) studies on natural deduction systems were basically restricted to (1) their use as a good deductive system for teaching logic, and (2) problems related to the formulation of the rules for the quantifiers, specially the rules corresponding to universal generalization and to existential instantiation. This situation changed dramatically when, in 1965, Dag Prawitz and Andrés Raggio proved, independently, the Normalization Theorem for classical first order logic. This had been left unproved by Gentzen in 1935.
In this course we want to show you how to use Natural Deduction for your own proofs and also how to prove its basic properties such as ``strong normalization" and confluence, as well as how to relate it to other kinds of proof systems, such as sequent calculi and labelled deduction. We also want to discuss the Curry-Howard correspondence, the beautiful connection to (functional) programming theory and some newer extensions of Natural Deduction to Linear and Modal logics.