Natural Deduction for the Working Logician: a slightly updated syllabus

1. Historical introduction: Jaśkowski and Gentzen
- Foundational context
- The first systems
- In what sense natural deduction is natural
- The year of 1965
2. Prawitz-style Natural Deduction (ND) and its properties
- Normalization
- Strong normalization
3. Other variants of Natural Deduction
4. Translations between systems and between logics
5. Natural Deduction for other logics
- Modal Logics
- Linear Logics
- The system Fat
- The ecumenical system
6.  Do it yourself Natural Deduction – Schematic Rules [what’s an
introduction rule? what’s an elimination rule?]
7. Natural Deduction and some relatives.
- Sequent Calculi
- Tableaux
8. Some advanced topics.
 

Natural Deduction for the Working Logician: a reader

A preliminary Reader for  the course.

[1]Francis Jeffry Pelletier, A Brief History of Natural Deduction, History and Philosophy of Logic 20 (1): 1-31, 1999

[2] Gerhrad Gentzen, Untersuchungen über das logische Schließen.I. Mathematische Zeitschrift [S.l.:s.n.] 39 (2): 176–210. 1934
 Untersuchungen über das logische Schließen. II. Mathematische Zeitschrift[S.l.: s.n.] 39 (3): 405–431. 1935

English translation in M. E. Szabo: Collected Papers of Gerhard Gentzen. North-Holland, 1969. Investigations into Logical Deduction

[3] Dag Prawitz, Natural Deduction: A Proof-Theoretical Study (Dover Books on Mathematics, 2006) original publication, Stockholm, 1965

[4] Sara Negri and Jan von Plato, Structural Proof Theory, CUP, 2001. Also Jan von Plato, Natural Deduction: Some Recent Developments 2003, from Negri's webpage.

[5] Jean-Yves Girard, Yves Lafont and Paul Taylor,  Proofs and Types, CUP, 1989.

[6]   Manipulating Proofs, Jonathan P. Seldin's manuscript, available from his publications page.

[7]  Curry’s anticipation of the types used inprogramming languages, Jonathan P. Seldin, Proceedings of the Annual Meeting of the Canadian Society for History and Philosophy of Mathematics, 2002. There are also slides available in his publications page.

[8] Propositional Logics Complexity and the Sub-Formula Property, Edward Hermann Haeusler, Proceedings Tenth International Workshop on Developments in Computational Models, Vienna, Austria, 13th July 2014,  Electronic Proceedings in Theoretical Computer Science, 179, pages 1-16, 2015.

NASSLLI 2016 is around the corner

Rutgers University is celebrating 250 years, yay! #RU250

NASSLLI 2016 (the North American Summer School on Logic, Language and Information 2016)
is happening there, pretty soon.

Together with Luiz Carlos Pereira and
Edward Hermann Haeusler I am teaching Natural Deduction for the Working Logician.

This blog is to provide some extra information about the course, like the reader for the first two lectures, which is the next post.

We plan to post the slides as well as exercise sheets. Feel free to contact us with questions!

Looking forward to meeting many logicians interested in Natural Deduction at NASSLLI!

Luiz Carlos, Hermann and Valeria