{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,29]],"date-time":"2024-07-29T13:59:29Z","timestamp":1722261569905},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"S5","license":[{"start":{"date-parts":[[2016,9,21]],"date-time":"2016-09-21T00:00:00Z","timestamp":1474416000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2016,9,21]],"date-time":"2016-09-21T00:00:00Z","timestamp":1474416000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["Schr275\/17-1"],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100003329","name":"Ministerio de Econom\u00eda y Competitividad","doi-asserted-by":"publisher","award":["FFI2013-46451-P"],"id":[{"id":"10.13039\/501100003329","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["Tr1112\/1-3"],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Synthese"],"published-print":{"date-parts":[[2021,3]]},"abstract":"Abstract<\/jats:title>In this paper we argue that an account of proof-theoretic harmony based on reductions and expansions delivers an inferentialist picture of meaning which should be regarded as intensional, as opposed to other approaches to harmony that will be dubbed extensional. We show how the intensional account applies to any connective whose rules obey the inversion principle first proposed by Prawitz and Schroeder-Heister. In particular, by improving previous formulations of expansions, we solve a problem with quantum-disjunction first posed by Dummett. As recently observed by Schroeder-Heister, however, the specification of an inversion principle cannot yield an exhaustive account of harmony. The reason is that there are more collections of elimination rules than just the one obtained by inversion which we are willing to acknowledge as being in harmony with a given collection of introduction rules. Several authors more or less implicitly suggest that what is common to all alternative harmonious collection of rules is their being interderivable with each other. On the basis of considerations about identity of proofs and formula isomorphism, we show that this is too weak a condition for a given collection of elimination rules to be in harmony with a collection of introduction rules, at least if the intensional picture of meaning we advocate is not to collapse on an extensional one.<\/jats:p>","DOI":"10.1007\/s11229-016-1200-3","type":"journal-article","created":{"date-parts":[[2016,9,21]],"date-time":"2016-09-21T16:20:13Z","timestamp":1474474813000},"page":"1145-1176","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":15,"title":["Proof-theoretic harmony: towards an intensional account"],"prefix":"10.1007","volume":"198","author":[{"ORCID":"http:\/\/orcid.org\/0000-0003-2844-129X","authenticated-orcid":false,"given":"Luca","family":"Tranchini","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,21]]},"reference":[{"issue":"6","key":"1200_CR1","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1093\/analys\/22.6.130","volume":"22","author":"ND Belnap","year":"1962","unstructured":"Belnap, N. D. (1962). Tonk, plonk and plink. Analysis, 22(6), 130\u2013134.","journal-title":"Analysis"},{"key":"1200_CR2","doi-asserted-by":"publisher","first-page":"477","DOI":"10.2178\/bsl\/1067620091","volume":"9","author":"K Do\u0161en","year":"2003","unstructured":"Do\u0161en, K. (2003). Identity of proofs based on normalization and generality. Bulletin of Symbolic Logic, 9, 477\u2013503.","journal-title":"Bulletin of Symbolic Logic"},{"key":"1200_CR3","volume-title":"Frege. Philosophy of language","author":"M Dummett","year":"1981","unstructured":"Dummett, M. (1981). Frege. Philosophy of language (2nd ed.). London: Duckworth.","edition":"2"},{"key":"1200_CR4","volume-title":"The logical basis of metaphysics","author":"M Dummett","year":"1991","unstructured":"Dummett, M. (1991). The logical basis of metaphysics. London: Duckworth."},{"key":"1200_CR5","unstructured":"Dyckhoff, R. (2016). Some remarks on proof-theoretic semantics. In T. Piecha & P. Schroeder-Heister (Eds.), Advances in proof-theoretic semantics. Trends in logic (Vol. 43, pp. 79\u201393). Cham: Springer."},{"key":"1200_CR6","first-page":"68","volume-title":"The collected papers of Gerhard Gentzen","author":"G Gentzen","year":"1953","unstructured":"Gentzen, G. (1953). Untersuchungen \u00fcber das logische Schlie\u00dfen, Mathematische Zeitschrift 39. Eng. transl. \u2018Investigations into logical deduction\u2019. In M. E. Szabo (Ed.), The collected papers of Gerhard Gentzen (pp. 68\u2013131). Amsterdam: North-Holland."},{"key":"1200_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-01539-1","volume-title":"Einf\u00fchrung in die operative Logik und Mathematik","author":"P Lorenzen","year":"1955","unstructured":"Lorenzen, P. (1955). Einf\u00fchrung in die operative Logik und Mathematik. Berlin: Springer."},{"key":"1200_CR8","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P. (1971). Hauptsatz for the intuitionistic theory of iterated inductive definitions. In J.\u00a0Fenstad (Ed.), Proceedings of the second scandinavian logic symposium. Studies in logic and the foundation of mathematics (Vol. 63, pp. 179\u2013216). Elsevier.","DOI":"10.1016\/S0049-237X(08)70847-4"},{"key":"1200_CR9","volume-title":"Intuitionistic type theory","author":"P Martin-L\u00f6f","year":"1984","unstructured":"Martin-L\u00f6f, P. (1984). Intuitionistic type theory. napoli: Bibliopolis."},{"issue":"2","key":"1200_CR10","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1080\/01445340701830334","volume":"29","author":"E Moriconi","year":"2008","unstructured":"Moriconi, E., & Tesconi, L. (2008). On inversion principles. History and Philosophy of Logic, 29(2), 103\u2013113.","journal-title":"History and Philosophy of Logic"},{"issue":"2","key":"1200_CR11","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1111\/theo.12051","volume":"81","author":"A Naibo","year":"2015","unstructured":"Naibo, A., & Petrolo, M. (2015). Are uniqueness and deducibility of identicals the same? Theoria, 81(2), 143\u2013181.","journal-title":"Theoria"},{"key":"1200_CR12","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511527340","volume-title":"Structural proof theory","author":"S Negri","year":"2001","unstructured":"Negri, S., & von Plato, J. (2001). Structural proof theory. Cambridge: Cambridge Univeristy Press."},{"issue":"1","key":"1200_CR13","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1017\/S1755020313000385","volume":"7","author":"GK Olkhovikov","year":"2014","unstructured":"Olkhovikov, G. K., & Schroeder-Heister, P. (2014). On flattening elimination rules. Review of Symbolic Logic, 7(1), 60\u201372.","journal-title":"Review of Symbolic Logic"},{"issue":"4","key":"1200_CR14","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1017\/S0960129501003322","volume":"11","author":"F Pfenning","year":"2001","unstructured":"Pfenning, F., & Davies, R. (2001). A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11(4), 511\u2013540.","journal-title":"Mathematical Structures in Computer Science"},{"key":"1200_CR15","unstructured":"Prawitz, D. (1965). Natural deduction. A proof-theoretical study. Stockholm: Almqvist & Wiksell. Reprinted in 2006 for Dover Publication."},{"key":"1200_CR16","doi-asserted-by":"crossref","unstructured":"Prawitz, D.: (1971). Ideas and results in proof theory. In J.\u00a0Fenstad (Ed.), Proceedings of the second scandinavian logic symposium. Studies in logic and the foundations of mathematics (Vol.63, pp. 235\u2013307). Elsevier.","DOI":"10.1016\/S0049-237X(08)70849-8"},{"key":"1200_CR17","unstructured":"Prawitz, D. (1979). Proofs and the meaning and completeness of the logical constants. In J. Hintikka, I. Niiniluoto, & E. Saarinen (Eds.), Essays on mathematical and philosophical logic: Proceedings of the fourth scandinavian logic symposium and the first soviet-finnish logic conference, Jyv\u00e4skyl\u00e4, Finland, June 29\u2013July 6, 1976 (pp. 25\u201340). Dordrecht: Kluwer."},{"issue":"2","key":"1200_CR18","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1093\/analys\/21.2.38","volume":"21","author":"AN Prior","year":"1960","unstructured":"Prior, A. N. (1960). The runabout inference-ticket. Analysis, 21(2), 38\u201339.","journal-title":"Analysis"},{"key":"1200_CR19","doi-asserted-by":"publisher","first-page":"557","DOI":"10.1007\/s10992-010-9133-7","volume":"39","author":"S Read","year":"2010","unstructured":"Read, S. (2010). General-elimination harmony and the meaning of the logical constants. Journal of Philosophical Logic, 39, 557\u201376.","journal-title":"Journal of Philosophical Logic"},{"key":"1200_CR20","unstructured":"Read, S. (2015). General-elimination harmony and higher-level rules. In H. Wansing (Ed.), Dag Prawitz on proofs and meaning. Outstanding contributions to logic (Vol. 7, pp. 293\u2013312). New York: Springer."},{"key":"1200_CR21","unstructured":"Schroeder-Heister, P. (1981). Untersuchungen zur regellogischen Deutung von Aussagenverkn\u00fcpfungen, Ph.D. thesis, Bonn University."},{"issue":"4","key":"1200_CR22","doi-asserted-by":"publisher","first-page":"1284","DOI":"10.2307\/2274279","volume":"49","author":"P Schroeder-Heister","year":"1984","unstructured":"Schroeder-Heister, P. (1984). A natural extension of natural deduction. The Journal of Symbolic Logic, 49(4), 1284\u20131300.","journal-title":"The Journal of Symbolic Logic"},{"issue":"1","key":"1200_CR23","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/s11245-012-9119-x","volume":"31","author":"P Schroeder-Heister","year":"2012","unstructured":"Schroeder-Heister, P. (2012). Proof-theoretic semantics, self-contradiction, and the format of deductive reasoning. Topoi, 31(1), 77\u201385.","journal-title":"Topoi"},{"issue":"6","key":"1200_CR24","doi-asserted-by":"publisher","first-page":"1185","DOI":"10.1007\/s11225-014-9562-3","volume":"102","author":"P Schroeder-Heister","year":"2014","unstructured":"Schroeder-Heister, P. (2014a). The calculus of higher-level rules, propositional quantification, and the foundational approach to proof-theoretic harmony. Studia Logica, 102(6), 1185\u20131216.","journal-title":"Studia Logica"},{"key":"1200_CR25","doi-asserted-by":"crossref","unstructured":"Schroeder-Heister, P. (2014b). Harmony in proof-theoretic semantics: A reductive analysis. Dag Prawitz on proofs and meaning. Outstanding contributions to logic (Vol. 7, pp. 329\u2013358). New York: Springer.","DOI":"10.1007\/978-3-319-11041-7_15"},{"issue":"3","key":"1200_CR26","doi-asserted-by":"publisher","first-page":"943","DOI":"10.1007\/s11229-011-9901-0","volume":"187","author":"G Sundholm","year":"2012","unstructured":"Sundholm, G. (2012). \u201cInference versus consequence\u201d revisited: inference, consequence, conditional, implication. Synthese, 187(3), 943\u2013956.","journal-title":"Synthese"},{"issue":"1","key":"1200_CR27","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1007\/s11245-012-9121-3","volume":"31","author":"L Tranchini","year":"2012","unstructured":"Tranchini, L. (2012). Proof from a proof-theoretic perspective. Topoi, 31(1), 47\u201357.","journal-title":"Topoi"},{"issue":"3","key":"1200_CR28","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1017\/S1755020315000179","volume":"8","author":"L Tranchini","year":"2015","unstructured":"Tranchini, L. (2015). Harmonising harmony. The Review of Symbolic Logic, 8(3), 495\u2013512.","journal-title":"The Review of Symbolic Logic"},{"issue":"2","key":"1200_CR29","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1093\/logcom\/exu028","volume":"26","author":"L Tranchini","year":"2016","unstructured":"Tranchini, L. (2016). Proof-theoretic semantics, paradoxes, and the distinction between sense and denotation. Journal of Logic and Computation, 26(2), 495\u2013512.","journal-title":"Journal of Logic and Computation"},{"key":"1200_CR30","unstructured":"Tranchini, L., Pistone, P. and Petrolo, M. n.d., The naturality of natural deduction. Under review."},{"key":"1200_CR31","volume-title":"Basic proof theory","author":"AS Troelstra","year":"1996","unstructured":"Troelstra, A. S., & Schwichtemberg, H. (1996). Basic proof theory. Cambridge: Cambridge University Press."},{"issue":"2","key":"1200_CR32","doi-asserted-by":"publisher","first-page":"240","DOI":"10.2178\/bsl\/1208442829","volume":"14","author":"J von Plato","year":"2008","unstructured":"von Plato, J. (2008). Gentzen\u2019s proof of normalization for natural deduction. Bulletin of Symbolic Logic, 14(2), 240\u2013257.","journal-title":"Bulletin of Symbolic Logic"}],"container-title":["Synthese"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11229-016-1200-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11229-016-1200-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11229-016-1200-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,30]],"date-time":"2021-03-30T10:26:10Z","timestamp":1617099970000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11229-016-1200-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,9,21]]},"references-count":32,"journal-issue":{"issue":"S5","published-print":{"date-parts":[[2021,3]]}},"alternative-id":["1200"],"URL":"https:\/\/doi.org\/10.1007\/s11229-016-1200-3","relation":{},"ISSN":["0039-7857","1573-0964"],"issn-type":[{"value":"0039-7857","type":"print"},{"value":"1573-0964","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,9,21]]},"assertion":[{"value":"8 October 2015","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"16 August 2016","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 September 2016","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}