Does the Implication Elimination Rule Need a Minor Premise?
DOI:
https://doi.org/10.12775/LLP.2017.019Keywords
natural deduction, NJ, proof-theoretic semantics, grounds for assertion, term assignmentAbstract
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.
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
Downloads
Published
How to Cite
Issue
Section
Stats
Number of views and downloads: 838
Number of citations: 0
