Proof Theory: Logical and Philosophical Aspects

This is an intensive class on logical and philosophical issues in proof theory, taught by Shawn Standefer and me at nasslli 2016. We cover cut elimination, some substructural logics, and hypersequents, with a bit of inferentialism and bilateralism mixed in. Here are the slides for each day of the course.

• Day 1: Foundations. An introduction to the sequent calculus for intuitionistic and classical logic, cut elimination and some of its consequences.
• Day 2: Substructural Logics. Structural rules in sequent systems; the case of distribution; different substructural logics and their applications; revisiting cut elimination in substructural logics.
• Day 3: Beyond Sequents. Sequent sytstems for basic modal logics; three ways to move beyond traditional sequent systems—display logic, labelled sequents and tree hypersequents.
• Day 4: Hypersequents for S5, Actuality and 2D Modal Logics. From tree hypersequents to simple hypersequents for S5; extending simple hypersequents to model actuality and two-dimensional modal logic.
• Day 5: Semantics. Normative pragmatics; the scope of rules and definitions; between proofs and models; moving beyond propositional logics.

Readings and References

Foundations

• Gerhard Gentzen, “Untersuchungen über das logische Schließen—I”, Mathematische Zeitschrift, 39(1):176–210, 1935.
• Gerhard Gentzen, The Collected Papers of Gerhard Gentzen, Translated and Edited by M. E. Szabo, North Holland, 1969.
• Albert Grigorevich Dragalin, Mathematical Intuitionism: Introduction to Proof Theory, American Mathematical Society, Translations of Mathematical Monographs, 1987.
• Roy Dyckhoff, “Contraction-Free Sequent Calculi for Intuitionistic Logic”, Journal of Symbolic Logic, 57:795–807, 1992.
• Sara Negri and Jan von Plato, Structural Proof Theory, Cambridge University Press, 2002.
• Katalin Bimbó, Proof Theory: Sequent Calculi and Related Formalisms, CRC Press, Boca Raton, FL, 2015
• Peter Milne, “Harmony, Purity, Simplicity and a ‘Seemingly Magical Fact’”, The Monist, 85(4):498–534, 2002

Substructural Logics

• Greg Restall, An Introduction to Substructural Logics, Routledge 2000.
• Francesco Paoli, Substructural Logics: A Primer, Springer 2002.
• Greg Restall, “Relevant and Substructural Logics”, pp. 289–396 in Logic and the Modalities in the Twentieth Century, Dov Gabbay and John Woods (editors), Elsevier 2006.
• Alan Ross Anderson and Nuel D. Belnap, Entailment: The Logic of Relevance and Necessity, Volume 1, Princeton University Press, 1975
• Alan Ross Anderson, Nuel D. Belnap and J. Michael Dunn, Entailment: The Logic of Relevance and Necessity, Volume 2, Princeton University Press, 1992
• Edwin D. Mares, Relevant Logic: A Philosophical Interpretation, Cambridge University Press, 2004
• J. Michael Dunn and Greg Restall, “Relevance Logic,” pp. 1–136 in The Handbook of Philosophical Logic, vol. 6, edition 2, Dov Gabbay and Franz Guenther (editors)
• Jean-Yves Girard, “Linear Logic,” Theoretical Computer Science, 50:1–101, 1987
• Jean-Yves Girard, Yves Lafont and Paul Taylor, Proofs and Types, Cambridge University Press, 1989
• Joachim Lambek, “The Mathematics of Sentence Structure,” American Mathematical Monthly, 65(3):154–170, 1958
• Glyn Morrill, Type Logical Grammar: Categorial Logic of Signs, Kluwer, 1994
• Johan van Benthem, Language in Action, North-Holland and MIT Press, 1995.
• Richard Moot and Christian Retoré, The Logic of Categorial Grammars, Springer 2012.
• Chris Barker, “Free Choice Permission as Resource-Sensitive Reasoning,” Semantics and Pragmatics, 3:10, 2010, 1-38.

Beyond Sequents

• Nuel D. Belnap, “Display Logic,” Journal of Philosophical Logic, 11:375–417, 1982.
• Heinrich Wansing, Displaying Modal Logic, Kluwer Academic Publishers, 1998.
• Sara Negri, “Proof Analysis in Modal Logic,” Journal of Philosophical Logic, 34:507–544, 2005.
• Arnon Avron, “Hypersequents, logical consequence and intermediate logics for concurrency,” Annals of Mathematics and Artificial intelligence, 4:225–248, 1991.
• Arnon Avron, “The method of hypersequents in the proof theory of propositional non-classical logics” in Logic: From Foundations to Applications, W. Hodges, et al., 1996, Oxford Science Publication, Oxford, pp. 1–32
• Francesca Poggiolesi, Gentzen Calculi for Modal Propositional Logic, Springer, 2011.
• Francesca Poggiolesi and Greg Restall, “Interpreting and Applying Proof Theory for Modal Logic,” New Waves in Philosophical Logic, ed. Greg Restall and Gillian Russell, Palgrave MacMillan, 2012.

Hypersequents for S5, Actuality and 2D Modal Logics

• Francesca Poggiolesi, “A Cut-Free Simple Sequent Calculus for Modal Logic S5,” Review of Symbolic Logic 1:1, 3–15, 2008.
• Greg Restall, “Proofnets for S5: sequents and circuits for modal logic,” Logic Colloquium 2005, ed. C. Dimitracopoulos, L. Newelski, D. Normann and J. R. Steel, Cambridge University Press, 2008.
• Kaja Bednarska and Andrzej Indrzejczak, “Hypersequent Calculi for S5: the methods of cut elimination” Logic and Logical Philosophy, 24, 277–311, 2015.
• Greg Restall, “A Cut-Free Sequent System for Two Dimensional Modal Logic, and why it matters,” Annals of Pure and Applied Logic, 163:11, 1611–1623, 2012.
• Martin Davies, “Reference, Contingency, and the Two-Dimensional Framework,” Philosophical Studies, 118(1):83–131, 2004.
• Martin Davies and Lloyd Humberstone, “Two Notions of Necessity,” Philosophical Studies, 38(1):1–30, 1980.
• Lloyd Humberstone, “Two-Dimensional Adventures,” Philosohical Studies, 118(1):257–277, 2004.

Semantics

• Arthur Prior, “The Runabout Inference Ticket.” Analaysis 21(2): 38–39, 1960.
• Nuel Belnap, “Tonk, Plonk and Plink,” Analysis, 22(6): 130–134, 1962.
• Nuel Nelnap “Declaratives Are Not Enough.” Philosophical Studies, 59(1): 1–30, 1990.
• Jaroslav Peregrin “An Inferentialist Approach to Semantics: Time for a New Kind of Structuralism?” Philosophy Compass, 3(6): 1208–1223, 2008.
• Greg Restall, “Multiple Conclusions” pp. 189–205 in Logic, Methodology and Philosophy of Science: Proceedings of the Twelfth International Congress, edited by P. Hájek, L. Valdés-Villanueva and D. Westerståhl, KCL Publications, 2005.
• Greg Restall, “Truth Values and Proof Theory” Studia Logica, 92(2):241–264, 2009.
• Raymond Smullyan, First-Order Logic. Springer-Verlag, 1968.
• Gaisi Takeuti, Proof Theory, 2nd edition. Elsevier, 1987.
• Michael Kremer “Kripke and the Logic of Truth.” Journal of Philosophical Logic, 17:225–278, 1988
• Sara Negri and Jan von Plato, Structural Proof Theory, Cambridge University Press, 2002.
• Greg Restall “Assertion, Denial and Non-Classical Theories.” In Paraconsistency: Logic and Applications, edited by Koji Tanaka, Francesco Berto, Edwin Mares and Francesco Paoli, pp. 81–99, 2013
• Anne Troelstra and Helmut Schwichtenberg, Basic Proof Theory, 2nd ed. Cambridge University Press, 2000.

Links

• nasslli 2016, Rutgers, July 2016.
• Class Proposal, containing our draft class outline.