{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:29:51Z","timestamp":1740122991183,"version":"3.37.3"},"reference-count":34,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2021,10,29]],"date-time":"2021-10-29T00:00:00Z","timestamp":1635465600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,10,29]],"date-time":"2021-10-29T00:00:00Z","timestamp":1635465600000},"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":["Tr1112\/4-1"],"award-info":[{"award-number":["Tr1112\/4-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[2022,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In a previous paper (of which this is a prosecution) we investigated the extraction of proof-theoretic properties of natural deduction derivations from their impredicative translation into System F. Our key idea was to introduce an extended equational theory for System F codifying at a syntactic level some properties found in parametric models of polymorphic type theory. A different approach to extract proof-theoretic properties of natural deduction derivations was proposed in a recent series of papers on the basis of an embedding of intuitionistic propositional logic into a predicative fragment of System F, called <jats:italic>atomic<\/jats:italic> System F. In this paper we show that this approach finds a general explanation within our equational study of second-order natural deduction, and a clear semantic justification in terms of parametricity.<\/jats:p>","DOI":"10.1007\/s11225-021-09964-z","type":"journal-article","created":{"date-parts":[[2021,10,29]],"date-time":"2021-10-29T13:03:54Z","timestamp":1635512634000},"page":"545-592","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["The Naturality of Natural Deduction (II): On Atomic Polymorphism and Generalized Propositional Connectives"],"prefix":"10.1007","volume":"110","author":[{"given":"Paolo","family":"Pistone","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2844-129X","authenticated-orcid":false,"given":"Luca","family":"Tranchini","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mattia","family":"Petrolo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,10,29]]},"reference":[{"key":"9964_CR1","doi-asserted-by":"crossref","unstructured":"Bainbridge, E.S., P. J. Freyd, A. Scedrov, and P. J. Scott, Functorial polymorphism, Theoretical Computer Science 70:35\u201364, 1990.","DOI":"10.1016\/0304-3975(90)90151-7"},{"key":"9964_CR2","doi-asserted-by":"publisher","first-page":"417","DOI":"10.1017\/S0956796800003750","volume":"10","author":"Gilles Barthe","year":"2000","unstructured":"Barthe, G., and M. H. S\u00f8rensen, Domain-free pure type systems, Journal of Functional Programming 10:417\u2013452, 2000.","journal-title":"Journal of Functional Programming"},{"key":"9964_CR3","first-page":"15","volume":"51","author":"Bruno Dinis","year":"2016","unstructured":"Dinis, B., and G. Ferreira, Instantiation overflow, Reports on Mathematical Logic 51:15\u201333, 2016.","journal-title":"Reports on Mathematical Logic"},{"issue":"4","key":"9964_CR4","doi-asserted-by":"publisher","first-page":"477","DOI":"10.2178\/bsl\/1067620091","volume":"9","author":"Kosta Do\u0161en","year":"2003","unstructured":"Do\u0161en, K., Identity of proofs based on normalization and generality, Bulletin of Symbolic Logic 9(4):477\u2013503, 2003.","journal-title":"Bulletin of Symbolic Logic"},{"key":"9964_CR5","doi-asserted-by":"crossref","unstructured":"Esp\u00edrito Santo, J., and G. Ferreira, A refined interpretation of intuitionistic logic by means of atomic polymorphism, Studia Logica 108:477\u2013507, 2020.","DOI":"10.1007\/s11225-019-09858-1"},{"key":"9964_CR6","doi-asserted-by":"crossref","unstructured":"Esp\u00edrito Santo, J., and G. Ferreira, The Russell-Prawitz embedding and the atomization of universal instantiation, Logic Journal of the IGPL 29(5):823\u2013858, 2021.","DOI":"10.1093\/jigpal\/jzaa025"},{"key":"9964_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10992-005-9001-z","volume":"35","author":"Fernando Ferreira","year":"2006","unstructured":"Ferreira. F., Comments on predicative logic, Journal of Philosophical Logic 35:1\u20138, 2006.","journal-title":"Journal of Philosophical Logic"},{"key":"9964_CR8","doi-asserted-by":"crossref","unstructured":"Ferreira, F., and G. Ferreira, Commuting conversions vs. the standard conversions of the \u201cgood\u201d connectives, Studia Logica 92(1):63\u201384, 2009.","DOI":"10.1007\/s11225-009-9186-1"},{"issue":"1","key":"9964_CR9","doi-asserted-by":"publisher","first-page":"260","DOI":"10.2178\/jsl.7801180","volume":"78","author":"Fernando Ferreira","year":"2013","unstructured":"Ferreira, F., and G. Ferreira, Atomic polymorphism, Journal of Symbolic Logic 78(1):260\u2013274, 2013.","journal-title":"Journal of Symbolic Logic"},{"key":"9964_CR10","unstructured":"Ferreira, F., and G. Ferreira, The faithfulness of atomic polymorphism, in Proceedings of Trends in Logic XIII, \u0141\u00f3dz University Press, 2014, pp. 55\u201365."},{"issue":"2","key":"9964_CR11","first-page":"115","volume":"25","author":"Gilda Ferreira","year":"2017","unstructured":"Ferreira, G., $$\\eta $$-conversions of IPC implemented in atomic F, Logic Journal of the IGPL 25(2):115\u2013130, 2017.","journal-title":"Logic Journal of the IGPL"},{"key":"9964_CR12","doi-asserted-by":"crossref","unstructured":"Gabbay, D., Semantical Investigations in Heyting\u2019s Intuitionistic Logic, Springer Science + Business, 1981.","DOI":"10.1007\/978-94-017-2977-2"},{"key":"9964_CR13","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1017\/S0305004112000394","volume":"154","author":"Nicola Gambino","year":"2013","unstructured":"Gambino, N., and J. Kock, Polynomial functors and polynomial monads, Mathematical Proceedings of the Cambridge Philosophical Society 154(1):153\u2013192, 2013.","journal-title":"Mathematical Proceedings of the Cambridge Philosophical Society"},{"key":"9964_CR14","doi-asserted-by":"crossref","unstructured":"Girard, J.-Y., A. Scedrov, and P. J. Scott, Normal forms and cut-free proofs as natural transformations, in Y. Moschovakis, (ed.), Logic from Computer Science, vol. 21 of Mathematical Sciences Research Institute Publications, Springer-Verlag, 1992, pp. 217\u2013241.","DOI":"10.1007\/978-1-4612-2822-6_8"},{"key":"9964_CR15","volume-title":"Proofs and Types","author":"Jean-Yves Girard","year":"1989","unstructured":"Girard J.-Y., Y. Lafont, and P. Taylor, Proofs and Types, Cambridge University Press, Cambridge, 1989."},{"issue":"1","key":"9964_CR16","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1016\/0890-5401(91)90053-5","volume":"93","author":"Daniel Leivant","year":"1991","unstructured":"Leivant, D., Finitely stratified polymorphism, Information and Computation 93(1):93\u2013113, 1991.","journal-title":"Information and Computation"},{"key":"9964_CR17","doi-asserted-by":"crossref","unstructured":"Lindley, S., Extensional rewriting with sums, in S. Ronchi Della Rocca, (ed.), Typed Lambda Calculi and Applications, TLCA 2007, vol. 4583 of Lecture Notes in Computer Science, Springer Verlag, 2007, pp. 255\u2013271.","DOI":"10.1007\/978-3-540-73228-0_19"},{"key":"9964_CR18","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1017\/S1755020313000385","volume":"7","author":"Grigory Olkhovikov","year":"2014","unstructured":"Olkhovikov, G., and P. Schroeder-Heister, On flattening elimination rules, The Review of Symbolic Logic 7:60\u201372, 2014.","journal-title":"The Review of Symbolic Logic"},{"key":"9964_CR19","unstructured":"Pistone, P., Proof nets and the instantiation overflow property, available atarXiv:1803.09297, 2018."},{"key":"9964_CR20","unstructured":"Pistone, P., and L. Tranchini, The Yoneda Reduction of Polymorphic Types, in Ch. Baier, and J. Goubault-Larrecq, (eds.), 29th EACSL Annual Conference on Computer Science Logic (CSL 2021), vol.183 of Leibniz International Proceedings in Informatics (LIPIcs), Dagstuhl, Germany, 2021, pp. 35:1\u201335:22"},{"key":"9964_CR21","unstructured":"Pistone, P., and L. Tranchini, What\u2019s Decidable about (Atomic) Polymorphism?, in N. Kobayashi, (ed.), Proceedings of Formal Structures of Computation and Deduction (FSCD 2021), vol. 195 of Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany, 2021, pp. 27:1\u201327:23."},{"key":"9964_CR22","unstructured":"Prawitz, D., Natural deduction, a proof-theoretical study, Almqvist & Wiskell, 1965."},{"key":"9964_CR23","doi-asserted-by":"crossref","unstructured":"Prawitz, D., Ideas and results in proof theory, in J.E. Fenstad, (ed.), Proceedings of the 2nd Scandinavian Logic Symposium (Oslo), vol. 63 of Studies in logic and foundations of mathematics, North-Holland, 1971, pp. 235\u2013307.","DOI":"10.1016\/S0049-237X(08)70849-8"},{"key":"9964_CR24","unstructured":"Prawitz, D., Proofs and the meaning and completeness of the logical constants, in J. Hintikka, I. Niiniluoto, and 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-July 6, 1976, Kluwer, Dordrecht, 1979, pp. 25\u201340."},{"key":"9964_CR25","unstructured":"Reynolds, J. C., Types, abstraction and parametric polymorphism, in R.E.A. Mason, (ed.), Information Processing \u201983, North-Holland, 1983, pp. 513\u2013523."},{"issue":"4","key":"9964_CR26","doi-asserted-by":"publisher","first-page":"1284","DOI":"10.2307\/2274279","volume":"49","author":"Peter Schroeder-Heister","year":"1984","unstructured":"Schroeder-Heister, P., A natural extension of natural deduction, Journal of Symbolic Logic 49(4):1284\u20131300, 1984.","journal-title":"Journal of Symbolic Logic"},{"key":"9964_CR27","unstructured":"Schwichtenberg, H., and A. S. Troelstra, Basic proof theory, Cambridge University Press, 2000."},{"key":"9964_CR28","doi-asserted-by":"crossref","unstructured":"Scherer, G., Deciding equivalence with sums and the empty type, in POPL 2017: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017, pp. 374\u2013386.","DOI":"10.1145\/3009837.3009901"},{"key":"9964_CR29","doi-asserted-by":"crossref","unstructured":"Seely, R.A.G.,Weak adjointness in proof theory, in Proceedings of the Durham Conference on Applications of Sheaves, vol. 753 of Springer Lecture Notes in Mathematics, Springer, Berlin, 1979, pp. 697\u2013701.","DOI":"10.1007\/BFb0061840"},{"issue":"1","key":"9964_CR30","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1007\/BF01147694","volume":"22","author":"SK Sobolev","year":"1977","unstructured":"Sobolev, S.K., The intuitionistic propositional calculus with quantifiers, Mathematical Notes 22(1):528\u2013532, 1977.","journal-title":"Mathematical Notes"},{"key":"9964_CR31","doi-asserted-by":"publisher","first-page":"1145","DOI":"10.1007\/s11229-016-1200-3","volume":"198","author":"Luca Tranchini","year":"2021","unstructured":"Tranchini, L., Proof-theoretic harmony: towards an intensional account. Synthese 198:1145\u20131176, 2021.","journal-title":"Synthese"},{"issue":"6","key":"9964_CR32","doi-asserted-by":"publisher","first-page":"1029","DOI":"10.1007\/s10992-018-9460-7","volume":"47","author":"Luca Tranchini","year":"2018","unstructured":"Tranchini, L., Stabilizing quantum disjunction, Journal of Philosophical Logic 47(6):1029\u20131047, 2018.","journal-title":"Journal of Philosophical Logic"},{"issue":"1","key":"9964_CR33","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s11225-017-9772-6","volume":"107","author":"Luca Tranchini","year":"2019","unstructured":"Tranchini, L., P. Pistone, and M. Petrolo, The naturality of natural deduction, Studia Logica 107(1):195\u2013231, 2019.","journal-title":"Studia Logica"},{"key":"9964_CR34","doi-asserted-by":"crossref","unstructured":"Wadler, P., Theorems for free!, in Proceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture, FPCA \u201989, ACM, New York, 1989, pp. 347\u2013359.","DOI":"10.1145\/99370.99404"}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-021-09964-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11225-021-09964-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-021-09964-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,21]],"date-time":"2022-03-21T11:32:55Z","timestamp":1647862375000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11225-021-09964-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,10,29]]},"references-count":34,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2022,4]]}},"alternative-id":["9964"],"URL":"https:\/\/doi.org\/10.1007\/s11225-021-09964-z","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[2021,10,29]]},"assertion":[{"value":"1 September 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 June 2021","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 October 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 February 2022","order":4,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Update","order":5,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The funding information \"Open Access funding enabled and organized by Projekt DEAL\" is included in the article.","order":6,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}}]}}