Proof-theoretic validity for sequents
Will Stafford
Keywords: proof-theoretic validity, classical logic, sequent calculus
Proof-theoretic validity offers a non-referential semantics for certain logics. Currently it has been developed for intuitionistic logic (e.g. [2]; [4]), certain intermediate logics (e.g. [3]; [5], and certain substructural logics (e.g. [1]). This has been done by using a natural deduction calculus. However, there are many logics that are more naturally represented in the sequence calculus, including, for the purposes of proof-theoretic validity, classical logic. This paper develops the beginnings of a notion of proof-theoretic validity for the sequent calculus and applies it to classical logic to show that in this setting the left rules for classical logic are valid given the right rules. We then address certain philosophical questions about this move including how we should interpret the sequence and whether this is a form of bilateralism.
Bibliography
- Gheorghiu, Alexander V., Tao Gu, and David J. Pym,Proof-Theoretic Semantics for Intuitionistic Multiplicative Linear Logic,Automated Reasoning with Analytic Tableaux and Related Methods(Prague),(Revantha Ramanayake and Josef Urban, editors),vol. 14278,Springer,2023,pp. 367–-385.
- Goldfarb, Warren,On Dummett’s ‘Proof-Theoretic Justifications of Logical Laws,Advances in Proof-Theoretic Semantics(Thomas Piecha and Peter Schroeder-Heister, editors),Springer,Cham,2016,pp. 195–210.
- Piecha, Thomas, Wagner de Campos Sanz, and Peter Schroeder-Heister,Failure of Completeness in Proof-Theoretic Semantics,Journal of Philosophical Logic,vol. 44 (2015), no. 3 pp. 321–-335.
- Stafford, Will and Victor Nascimento,Following all the rules: Intuitionistic completeness for generalized proof-theoretic validity,Analysis,vol. 83 (2023), no. 3, pp. 507–-516.
- Stafford, Will,Proof-Theoretic Semantics and Inquisitive Logic,Journal of Philosophical Logic,vol. 50 (2021), no. 5, pp. 1199-–1229.