Geodesic
Structural Rules in Natural Deduction with Alternatives
Bulletin of the Section of Logic, Tome 52 (2023) no. 2, pp. 109-143

Voir la notice de l'article provenant de la source Library of Science

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.
Keywords: proof, natural deduction, classical logic, bilateralism, substructural logics 
Restall, Greg. Structural Rules in Natural Deduction with Alternatives. Bulletin of the Section of Logic, Tome 52 (2023) no. 2, pp. 109-143. http://geodesic.mathdoc.fr/item/BSL_2023_52_2_a0/
@article{BSL_2023_52_2_a0,
     author = {Restall, Greg},
     title = {Structural {Rules} in {Natural} {Deduction} with {Alternatives}},
     journal = {Bulletin of the Section of Logic},
     pages = {109--143},
     year = {2023},
     volume = {52},
     number = {2},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/BSL_2023_52_2_a0/}
}
TY  - JOUR
AU  - Restall, Greg
TI  - Structural Rules in Natural Deduction with Alternatives
JO  - Bulletin of the Section of Logic
PY  - 2023
SP  - 109
EP  - 143
VL  - 52
IS  - 2
UR  - http://geodesic.mathdoc.fr/item/BSL_2023_52_2_a0/
LA  - en
ID  - BSL_2023_52_2_a0
ER  - 
%0 Journal Article
%A Restall, Greg
%T Structural Rules in Natural Deduction with Alternatives
%J Bulletin of the Section of Logic
%D 2023
%P 109-143
%V 52
%N 2
%U http://geodesic.mathdoc.fr/item/BSL_2023_52_2_a0/
%G en
%F BSL_2023_52_2_a0

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

[2] 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.

[3] J.-Y. Girard, Linear Logic, Theoretical Computer Science, vol. 50 (1987), pp. 1–101 | DOI

[4] L. Incurvati, P. Smith, Rejection and valuations, Analysis, vol. 70(1) (2010), pp. 3–10 | DOI

[5] D. Leivant, Assumption Classes in Natural Deduction, Mathematical Logic Quarterly, vol. 25(1–2) (1979), pp. 1–4 | DOI

[6] S. Negri, A normalizing system of natural deduction for intuitionistic linear logic, Archive for Mathematical Logic, vol. 41(8) (2002), pp. 789–810 | DOI

[7] F. Paoli, Substructural Logics: A Primer, Springer (2002) | DOI

[8] 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

[9] 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

[10] 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

[11] D. Prawitz, Natural Deduction: A Proof Theoretical Study, Almqvist and Wiksell, Stockholm (1965).

[12] G. Restall, An Introduction to Substructural Logics, Routledge (2000).

[13] 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.

[14] 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.

[15] E. Robinson, Proof Nets for Classical Logic, Journal of Logic and Computation, vol. 13(5) (2003), pp. 777–797 | DOI

[16] I. Rumfitt, "Yes" and "No", Mind, vol. 109(436) (2000), pp. 781–823 | DOI

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

[18] D. J. Shoesmith, T. J. Smiley, Multiple-Conclusion Logic, Cambridge University Press, Cambridge (1978) | DOI

[19] T. Smiley, Rejection, Analysis, vol. 56 (1996), pp. 1–9 | DOI

[20] N. Tennant, Natural Logic, Edinburgh University Press, Edinburgh (1978).

[21] A. S. Troelstra, Lectures on Linear Logic, csli Publications (1992).

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

[23] E. Zimmermann, Substructural Logics in Natural Deduction, Logic Journal of IGPL, vol. 15(3) (2007), pp. 211–232 | DOI