Abstract
The paper studies the extension of harmony and stability, major themes in proof-theoretic semantics, from single-conclusion natural-deduction systems to multiple-conclusions natural-deduction, independently of classical logic. An extension of the method of obtaining harmoniously-induced general elimination rules from given introduction rules is suggested, taking into account sub-structurality. Finally, the reductions and expansions of the multiple-conclusions natural-deduction representation of classical logic are formulated.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Blamey S., Humberstone L.: A perspective on modal sequent logic. Publ. RIMS Kyoto Univ. 27, 763–782 (1991)
Boric̆ić B.: On sequence-conclusion natural-deduction systems. J. Philos. Log. 14, 359–377 (1985)
Boric̆ić B.: On certain normalizable natural deduction formulations of some propositional intermediate logics. Notre Dame J. Form. Log. 29(4), 563–568 (1988)
Boric̆ić, B., Ilic̆, M.: An alternative normalisation of the implicative fragment of classical logic. Stud. Log. (2014, to appear)
Cellucci C.: Existential instantiation and normalization in sequent natural deduction. Ann. Pure Appl. Log. 58, 111–148 (1992)
Davies R., Pfenning F.: A modal analysis of staged computation. J. ACM 48(3), 555–604 (2001)
Dos̆en K.: Logical constants as punctuation marks. Notre Dame J. Form. Log. 30(3), 362–381 (1989)
Dummett, M.: The Logical Basis of Metaphysics. Harvard University Press, Cambridge (1993) (paperback). Hard copy (1991)
Francez, N.: Relevant harmony. J. Log. Comput. (2013) doi:10.1093/logcom/ext026. Special issue Logic: Between Semantics and Proof Theory, in honor of Arnon Avron’s 60th birthday
Francez, N.: Views of proof-theoretic semantics: Reified proof-theoretic meanings. J. Comput. Log. (2014, to appear). Special issue in honour of Roy Dyckhoff
Francez N., Ben-Avi G.: Proof-theoretic semantic values for logical operators. Rev. Symb. Log. 4(3), 337–485 (2011)
Francez N., Dyckhoff R.: Proof-theoretic semantics for a natural language fragment. Linguist. Philos. 33(6), 447–477 (2010)
Francez N., Dyckhoff R.: A note on harmony. J. Philos. Log. 41(3), 613–628 (2012)
Francez N., Dyckhoff R., Ben-Avi G.: Proof-theoretic semantics for subsentential phrases. Stud. Log. 94, 381–401 (2010)
Gentzen, G.: The consistency of elementary number theory. In: Szabo, M.E. (ed.) The collected papers of Gerhard Gentzen, pp. 493–565. North-Holland, Amsterdam (1935). English translation of the 1935 paper in Mathematische Annalen (in German)
Gentzen, G.: Investigations into logical deduction. In: Szabo, M.E. (ed.) The collected papers of Gerhard Gentzen, pp. 68–131. North-Holland, Amsterdam (1935). English translation of the 1935 paper in German
Girard J.-Y.: Linear logic. Theor. Comput. Sci. 50, 1–102 (1987)
Hjortland, O.T.: The Structure of Logical Consequence: Proof-Theoretic Conceptions. PhD thesis, University of St Andrews, (2009)
Hjortland, O.T.: Harmony and the context of deducibility. In: Novaes C.D., Hjortland, O.T. (eds.) Insolubles and Consequences: Essays in Honour of Stephen Read, pp. 135–154. College Publications, London 2013
Humberstone, L.: The Connectives. MIT Press, Cambridge (2011)
Milne P.: Classical harmony: rules of inference and the meaning of the logical constants. Synthese 100(1), 49–94 (1994)
Moriconi E., Tesconi L.: On inversion principles. Hist. Philos. Log. 29(2), 103–113 (2008)
Negri S.: Varieties of linear calculi. J. Philos. Log. 32(6), 569–590 (2002)
Negri S., von Plato J.: Sequent calculus in natural deduction style. J. Symb. Log. 66(4), 1803–1816 (2001)
Olkhovikov, G.K., Schroeder-Heister, P.: On flattening general elimination rules. Rev. Symb. Log. 7(1), (2014)
Pfenning F., Davies R.: A judgmental reconstruction of modal logic. Math. Struct. Comput. Sci. 11, 511–540 (2001)
Prawitz, D.: Natural Deduction: A Proof-Theoretical Study. Almqvist and Wicksell, Stockholm (1965). Soft cover edition by Dover, 2006
Prawitz, D.: Ideas and results in proof theory. In: Fenstad, J. (ed.) Proceedings of the 2nd Scandinavian Symposium. North-Holland, Amsterdam (1971)
Prawitz, D.: Proofs and the meaning and completeness of logical constants. In: Hintikka, J., Niiniluoto, I., Saarinen, E. (eds.) Essays in Mathematical and Philosophical Logic, pp. 25–40. Reidel, Dordrecht (1978)
Prior A.N.: The runabout inference-ticket. Analysis, 21, 38–39 (1960)
Read S.: Harmony and autonomy in classical logic. J. Philos. Log. 29, 123–154 (2000)
Read S.: General-elimination harmony and the meaning of the logical constants. J. Philos. Log. 39, 557–576 (2010)
Read, S.: General elimination harmony and higher-level rules. In: Wansing, H. (ed.) Dag Prawitz on Proofs and Meaning. Springer, Berlin (2014). Studia Logica Outstanding contributions to logic series
Restall, G.: Multiple conclusions. In: In 12th International Congress on Logic, Methodology and Philosophy of Science, pp. 189–205 (2005)
Rumfitt I.: ‘yes’ and ‘no’. Mind 169(436, 781–823), 169–436, 781823 (2000)
Sandqvist, T.: Acceptance, inference, and the multiple-conclusion sequent. Synthese (2011). doi:10.1007/s11229-011-9909-5
Schroeder-Heister, P.: The calculus of higher-level rules, propositional quantification, and the foundational approach to proof-theoretic harmony. In: Indrzejczak, A. (ed.) Gentzen’s and Jaśkowski’s Heritage: 80 Years of Natural Deduction and Sequent Calculi (2014). Special issue of Studia Logica
Schroeder-Heister, P.: Harmony in proof-theoretic semantics: a reductive analysis. In: Wansing, H. (ed.) Dag Prawitz on Proofs and Meaning. Springer, Berlin (2014). Studia Logica Outstanding contributions to logic series
Steinberger F.: Why conclusions should remain single. J. Philos. Log. 40, 333–355 (2011)
Tennant, N.: The Taming of the True. Oxford University Press, Oxford (1997)
Tesconi, L.: A Strong Normalization Theorem for natural deduction with general elimination rules. PhD thesis, University of Pisa (2004)
von Plato J.: Natural deduction with general elimination rules. Arch. Math. Log. 40, 541–567 (2001)
Wadler P.: There is no substitute for linear logic. In: 8th International Workshop on Mathematical Foundations of Programming Semantics. Oxford, UK (1992)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Francez, N. Harmony in Multiple-Conclusion Natural-Deduction. Log. Univers. 8, 215–259 (2014). https://doi.org/10.1007/s11787-014-0103-7
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11787-014-0103-7