Structural Rules in Natural Deduction with Alternatives

Greg Restall

doi:10.18778/0138-0680.2023.6

Authors

Greg Restall University of St Andrews, Department of Philosophy, Edgecliffe, The Scores, Scotland, UK

DOI:

https://doi.org/10.18778/0138-0680.2023.6

Keywords:

proof, natural deduction, classical logic, bilateralism, substructural logics

Abstract

Natural deduction with alternatives extends Gentzen–Prawitz-style natural deduction with a single structural addition: negatively signed assumptions, called alternatives. It is a mildly bilateralist, single-conclusion natural deduction proof system in which the connective rules are unmodi_ed from the usual Prawitz introduction and elimination rules — the extension is purely structural. This framework is general: it can be used for (1) classical logic, (2) relevant logic without distribution, (3) affine logic, and (4) linear logic, keeping the connective rules fixed, and varying purely structural rules.

The key result of this paper is that the two principles that introduce kinds of irrelevance to natural deduction proofs: (a) the rule of explosion (from a contradiction, anything follows); and (b) the structural rule of vacuous discharge; are shown to be two sides of a single coin, in the same way that they correspond to the structural rule of weakening in the sequent calculus. The paper also includes a discussion of assumption classes, and how they can play a role in treating additive connectives in substructural natural deduction.

References

H. B. Curry, R. Feys, Combinatory Logic, vol. 1, North Holland (1958).
Google Scholar

M. J. Gabbay, M. J. Gabbay, Some Formal Considerations on Gabbay's Restart Rule in Natural Deduction and Goal-Directed Reasoning, [in:] S. Artemov, H. Barringer, A. S. d'Avila Garcez, L. C. Lamb, J. Woods (eds.), We Will Show Them: Essays in Honour of Dov Gabbay, vol. 1, College Publications (2005), pp. 701–730.
Google Scholar

J.-Y. Girard, Linear Logic, Theoretical Computer Science, vol. 50 (1987), pp. 1–101, DOI: https://doi.org/10.1016/0304-3975(87)90045-4
Google Scholar DOI: https://doi.org/10.1016/0304-3975(87)90045-4

L. Incurvati, P. Smith, Rejection and valuations, Analysis, vol. 70(1) (2010), pp. 3–10, DOI: https://doi.org/10.1093/analys/anp134
Google Scholar DOI: https://doi.org/10.1093/analys/anp134

D. Leivant, Assumption Classes in Natural Deduction, Mathematical Logic Quarterly, vol. 25(1–2) (1979), pp. 1–4, DOI: https://doi.org/10.1002/malq.19790250102
Google Scholar DOI: https://doi.org/10.1002/malq.19790250102

S. Negri, A normalizing system of natural deduction for intuitionistic linear logic, Archive for Mathematical Logic, vol. 41(8) (2002), pp. 789–810, DOI: https://doi.org/10.1007/s001530100136
Google Scholar DOI: https://doi.org/10.1007/s001530100136

F. Paoli, Substructural Logics: A Primer, Springer (2002), DOI: https://doi.org/10.1007/978-94-017-3179-9
Google Scholar DOI: https://doi.org/10.1007/978-94-017-3179-9

M. Parigot, λμ-Calculus: An Algorithmic Interpretation of Classical Natural Deduction, [in:] A. Voronkov (ed.), International Conference on Logic for Programming Artificial Intelligence and Reasoning, vol. 624 of Lecture Notes in Artificial Intelligence, Springer (1992), pp. 190–201, DOI: https://doi.org/10.1007/BFb0013061
Google Scholar DOI: https://doi.org/10.1007/BFb0013061

M. Parigot, Classical proofs as programs, [in:] G. Gottlob, A. Leitsch, D. Mundici (eds.), Computational Logic and Proof Theory, vol. 713 of Lecture Notes in Computer Science, Springer (1993), pp. 263–276, DOI: https://doi.org/10.1007/BFb0022575
Google Scholar DOI: https://doi.org/10.1007/BFb0022575

M. Parigot, Proofs of Strong Normalisation for Second Order Classical Natural Deduction, The Journal of Symbolic Logic, vol. 62(4) (1997), pp. 1461–1479, DOI: https://doi.org/10.2307/2275652
Google Scholar DOI: https://doi.org/10.2307/2275652

D. Prawitz, Natural Deduction: A Proof Theoretical Study, Almqvist and Wiksell, Stockholm (1965).
Google Scholar

G. Restall, An Introduction to Substructural Logics, Routledge (2000).
Google Scholar

G. Restall, Multiple Conclusions, [in:] P. Hájek, L. Valdés-Villanueva, D. Westerståhl (eds.), Logic, Methodology and Philosophy of Science: Proceedings of the Twelfth International Congress, KCL Publications (2005), pp. 189–205.
Google Scholar

G. Restall, Proofnets for s5: Sequents and circuits for modal logic, [in:] C. Dimitracopoulos, L. Newelski, D. Normann (eds.), Logic Colloquium 2005, vol. 28 of Lecture Notes in Logic, Cambridge University Press (2007), pp. 151–172.
Google Scholar DOI: https://doi.org/10.1017/CBO9780511546464.012

E. Robinson, Proof Nets for Classical Logic, Journal of Logic and Computation, vol. 13(5) (2003), pp. 777–797, DOI: https://doi.org/10.1093/logcom/13.5.777
Google Scholar DOI: https://doi.org/10.1093/logcom/13.5.777

I. Rumfitt, "Yes" and "No", Mind, vol. 109(436) (2000), pp. 781–823, DOI: https://doi.org/10.1093/mind/109.436.781
Google Scholar DOI: https://doi.org/10.1093/mind/109.436.781

M. Schönfinkel, Über die Bausteine der mathematischen Logik, Mathematische Annallen, vol. 92 (1924), pp. 305–316, DOI: https://doi.org/10.1007/BF01448013, translated and reprinted as “On the Building Blocks of Mathematical Logic” in From Frege to Gödel [22].
Google Scholar DOI: https://doi.org/10.1007/BF01448013

D. J. Shoesmith, T. J. Smiley, Multiple-Conclusion Logic, Cambridge University Press, Cambridge (1978), DOI: https://doi.org/10.1017/CBO9780511565687
Google Scholar DOI: https://doi.org/10.1017/CBO9780511565687

T. Smiley, Rejection, Analysis, vol. 56 (1996), pp. 1–9, DOI: https://doi.org/10.1111/j.0003-2638.1996.00001.x
Google Scholar DOI: https://doi.org/10.1093/analys/56.1.1

N. Tennant, Natural Logic, Edinburgh University Press, Edinburgh (1978).
Google Scholar

A. S. Troelstra, Lectures on Linear Logic, csli Publications (1992).
Google Scholar

J. van Heijenoort, From Frege to Gödel: a source book in mathematical logic, 1879–1931, Harvard University Press, Cambridge, Mass. (1967).
Google Scholar

E. Zimmermann, Substructural Logics in Natural Deduction, Logic Journal of IGPL, vol. 15(3) (2007), pp. 211–232, DOI: https://doi.org/10.1093/jigpal/jzm008
Google Scholar DOI: https://doi.org/10.1093/jigpal/jzm008