Does the Implication Elimination Rule Need a Minor Premise?

• Authors: Francez Nissim
• Languages of publication: EN

Abstracts

EN

The paper introduces NJ g , a variant of Gentzen’s NJ natural deduction system, in which the implication elimination rule has no minor premise. The NJ g -systems extends traditional ND-system with a new kind of action in derivations, assumption incorporation, a kind of dual to the assumption discharge action. As a result, the implication (I/E)-rules are invertible and, almost by definition, harmonious and stable, a major condition imposed by proof-theoretic semantics on ND-systems to qualify as meaning-conferring. There is also a proof-term assignment to NJ g -derivations, materialising the Curry-Howard correspondence for this system.

Keywords

EN

natural deduction; NJ; proof-theoretic semantics; grounds for assertion; term assignment

• Publisher: Uniwersytet Mikołaja Kopernika (Nicolaus Copernicus University in Toruń)
• Journal: Logic and Logical Philosophy
• Year: 2018
• Volume: 27
• Issue: 3
• Pages: 351-373

Dates

published

2018-09-15

Contributors

author

Francez Nissim

• Computer Science Department the Technion-IIT Haifa, Israel

References

• Avron, A., “Simple consequence relations”, Information and Computation 92, 1 (1991): 105–139. DOI: 10.1016/0890-5401(91)90023-U
• Dočsen, K., “Logical constants as punctuation marks”, Notre Dame Journal of Formal Logic 30, 3 (1989): 362–381. PDF: https://projecteuclid.org/download/pdf_1/euclid.ndjfl/1093635154
• Dummett, M., The Logical Basis of Metaphysics, Harvard University Press, Cambridge, MA., 1993 (paperback); hard copy 1991.
• Francez, N., Proof-theoretic Semantics, College Publications, London, 2015.
• Francez, N., “Relevant harmony”, Journal of Logic and Computation 26, 1 (2016): 235–245. Special issue Logic: Between Semantics and Proof Theory, in honor of Arnon Avron’s 60th birthday. DOI: 10.1093/logcom/ext026
• Francez, N., “Views of proof-theoretic semantics: Reified proof-theoretic meanings”, Journal of Computational Logic 26, 2 (2016): 479–494. Special issue in honour of Roy Dyckhoff. DOI: 10.1093/logcom/exu035
• Gentzen, G., “The consistency of elementary number theory”, pages 493–565 in M.E. Szabo (ed.), The Collected Papers of Gerhard Gentzen, North-Holland, Amsterdam, 1935. English translation of the 1935 paper in Mathematische Annalen (in German).
• Gentzen, G., “Investigations into logical deduction”, pages 68–131 in M.E. Szabo (ed.), The Collected Papers of Gerhard Gentzen, North-Holland, Amsterdam, 1935. English translation of the 1935 paper in German.
• Hazen, A.P., and F.J. Pelletier, “Gentzen and Jaśkowski natural deduction: Fundamentally similar but importantly different”, Studia Logica 102, 6 (2014): 1–40. Special Issue: “Gentzen’s and Jaśkowski’s Heritage 80 Years of Natural Deduction and Sequent Calculi”, edited by A. Indrzejczak. DOI: 10.1007/s11225-014-9564-1
• Hindley, J.R., Basic Simple Type Theory, Cambridge University Press, 1997. DOI: 10.1017/CBO9780511608865
• Hitzmann, J., “Semantic partition and the ambiguity of sentences containing temporal adverbials”, J. of Semantics, in press, 1997.
• Jacinto, B., and S. Read, “General-elimination stability”, Studia Logica 105, 2 (2017): 361–405. DOI: 10.1007/s11225-016-9692-x
• Jaśkowski, S., “Teoria dedukcji oparta na regułach założeniowych” (Theory of deduction based on suppositional rules), page 36 in Księga pamiątkowa pierwszego polskiego zjazdu matematycznego (Proceedings of the First Polish Mathematical Congress), Polish Mathematical Society, Kraków, 1929.
• Jaśkowski, S., “On the rules of suppositions in formal logic”, Studia Logica, 1 (1936): 5–32. Reprinted: pages 232–258 in S. McCall, Polish Logic 1920–1939, Oxford UP, 1967.
• Johansson, I., “Der minimalkalkül, ein reduzierter intuitionistischer formalismus”, Compositio Mathematica 4 (1936): 119–136.
• Negri, S., and J. von Plato, Structural Proof Theory, CambridgeUniversity Press, Cambridge, UK, 2001. DOI: 10.1017/CBO9780511527340
• Prawitz, D., Natural Deduction: A Proof-Theoretical Study, Almqvist and Wicksell, Stockholm, 1965. Soft cover edition by Dover, 2006.
• Prawitz, D., “Meaning approached via proofs”, Synthese 148, 3 (2006): 507–524. DOI: 10.1007/s11229-004-6295-2
• Prawitz, D., “Explaining deductive inference”, pages 233–248 in H. Wansing (ed.), Dag Prawitz on proofs and meaning, Springer, 2014. Volume 7 of the series “Outstanding Contributions to Logic”. DOI: 10.1007/978-3-319-11041-7_3
• Schroeder-Heister, P., “A natural extension of natural deduction”, Journal of Symbolic Logic 49, 4 (1984): 1284–1300. DOI: 10.2307/2274279
• Schroeder-Heister, P., “On the notion of assumption in logical systems”, in R. Bluhm and C. Nimtz (eds.), Philosophy-Science-Scientific Philosophy, Mentis, Paderborn, 2004. Selected papers of the 5th int. congress of the society for Analytic Philosophy, Bielfield, September 2003.
• Schroeder-Heister, P., “The categorical and the hypothetical: A critique of some fundamental assumptions of standard semantics”, Synthese 187, 3 (2012): 925–942. DOI: 10.1007/s11229-011-9910-z
• Schroeder-Heister, P., “Proof-theoretic semantics”, in E.N. Zalta (ed.), The Stanford Encyclopedia of Philosophy, Spring 2013 edition, 2013. https://plato.stanford.edu/archives/win2016/entries/proof-theoretic-semantics/
• Scott, D., “Rules and derived rules”, pages 101–118 in S. Stenlund (ed.), Logical Theory and Semantic Analysis, Reidl, Dordrecht, 1974. DOI: 10.1007/978-94-010-2191-3_13