{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,22]],"date-time":"2026-04-22T20:12:01Z","timestamp":1776888721095,"version":"3.51.2"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2024,5,3]],"date-time":"2024-05-03T00:00:00Z","timestamp":1714694400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,5,3]],"date-time":"2024-05-03T00:00:00Z","timestamp":1714694400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/S013008\/1"],"award-info":[{"award-number":["EP\/S013008\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[2025,2]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>In proof-theoretic semantics, model-theoretic validity is replaced by proof-theoretic validity. Validity of formulae is defined inductively from a base giving the validity of atoms using inductive clauses derived from proof-theoretic rules. A key aim is to show completeness of the proof rules without any requirement for formal models. Establishing this for propositional intuitionistic logic raises some technical and conceptual issues. We relate Sandqvist\u2019s (complete) base-extension semantics of intuitionistic propositional logic to categorical proof theory in presheaves, reconstructing categorically the soundness and completeness arguments, thereby demonstrating the naturality of Sandqvist\u2019s constructions. This naturality includes Sandqvist\u2019s treatment of disjunction that is based on its second-order or elimination-rule presentation. These constructions embody not just validity, but certain forms of objects of justifications. This analysis is taken a step further by showing that from the perspective of validity, Sandqvist\u2019s semantics can also be viewed as the natural disjunction in a category of sheaves.<\/jats:p>","DOI":"10.1007\/s11225-024-10101-9","type":"journal-article","created":{"date-parts":[[2024,5,3]],"date-time":"2024-05-03T08:02:16Z","timestamp":1714723336000},"page":"125-162","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Categorical Proof-theoretic Semantics"],"prefix":"10.1007","volume":"113","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6504-5838","authenticated-orcid":false,"given":"David","family":"Pym","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-2100-8866","authenticated-orcid":false,"given":"Eike","family":"Ritter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3075-2217","authenticated-orcid":false,"given":"Edmund","family":"Robinson","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,5,3]]},"reference":[{"key":"10101_CR1","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1016\/j.tcs.2006.08.002","volume":"364","author":"G Bellin","year":"2006","unstructured":"Bellin, G., H. Martin, and P. Edmund, Robinson, and Christian Urban Categorical proof theory of classical propositional calculus, Theoretical Computer Science, 364:146\u2013165, 2006.","journal-title":"Theoretical Computer Science"},{"key":"10101_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic","author":"P Blackburn","year":"2001","unstructured":"Blackburn, P., M. de Rijke, and Y. Venema, Modal Logic, Cambridge University Press, 2001."},{"key":"10101_CR3","volume-title":"Logic and Structure","author":"D van Dalen","year":"2012","unstructured":"van Dalen, D., Logic and Structure, Springer, Cham, 5th edition, 2012.","edition":"5"},{"key":"10101_CR4","volume-title":"The Logical Basis of Metaphysics","author":"Michael Dummett","year":"1993","unstructured":"Dummett, M., The Logical Basis of Metaphysics, Harvard University Press, 1993."},{"key":"10101_CR5","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/s11225-019-09858-1","volume":"108","author":"J Espirito Santo","year":"2020","unstructured":"Espirito Santo, J., and G. Ferreira, A refined interpretation of intuitionistic logic by means of atomic polymorphism, Studia Logica 108:477\u2013507, 2020.","journal-title":"Studia Logica"},{"key":"10101_CR6","doi-asserted-by":"crossref","unstructured":"Ferreira, F., Comments on predicative logic, Journal of Philosophical Logic 35(1):1\u20138, 2006.","DOI":"10.1007\/s10992-005-9001-z"},{"key":"10101_CR7","unstructured":"Ferreira, F., and G. Ferreira, The faithfulness of atomic polymorphism, in A. Indrzejczak, J. Kaczmarek, and M. Zawidzki, (eds.), Proceedings of Trends in Logic XIII, \u0141\u00f3d\u017a University Press, L\u00f3d\u017a, 2014, pp. 55\u201365."},{"issue":"1","key":"10101_CR8","doi-asserted-by":"publisher","first-page":"260","DOI":"10.2178\/jsl.7801180","volume":"78","author":"F Ferreira","year":"2013","unstructured":"Ferreira, F., and G. Ferreira, Atomic polymorphism. The Journal of Symbolic Logic 78(1):260\u2013274, 2013.","journal-title":"The Journal of Symbolic Logic"},{"issue":"6","key":"10101_CR9","doi-asserted-by":"publisher","first-page":"1301","DOI":"10.1007\/s11225-015-9620-5","volume":"103","author":"F Ferreira","year":"2015","unstructured":"Ferreira, F., and G. Ferreira, The faithfulness of fat: a proof-theoretic proof, Studia Logica 103(6): 1301, 2015.","journal-title":"Studia Logica"},{"issue":"1","key":"10101_CR10","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.jpaa.2005.03.016","volume":"204","author":"C F\u00fchrmann","year":"2006","unstructured":"F\u00fchrmann, C., and D. Pym, Order-enriched categorical models of the classical sequent calculus, Journal of Pure and Applied Algebra 204(1):21\u201378, 2006.","journal-title":"Journal of Pure and Applied Algebra"},{"key":"10101_CR11","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1007\/BF01201363","volume":"39","author":"G Gentzen","year":"1935","unstructured":"Gentzen, G., Untersuchungen \u00dcber Das Logische Schlie\u00dfen. II. Mathematische Zeitschrift 39:405\u2013431, 1935.","journal-title":"II. Mathematische Zeitschrift"},{"key":"10101_CR12","unstructured":"Gheorghiu, A. V., and D. J. Pym, From Proof-theoretic Validity to Base-extension Semantics for Intuitionistic Propositional Logic. https:\/\/arxiv.org\/pdf\/2210.05344, 2022. Submitted."},{"key":"10101_CR13","unstructured":"Girard, J.Y., Interpr\u00e9tation fonctionnelle et \u00e9limination des coupures de l\u2019arithm\u00e9tique d\u2019ordre sup\u00e9rieur. Th\u00e8se de Doctorat d\u2019Etat, Universit\u00e9 Paris VII, 1972."},{"key":"10101_CR14","volume-title":"Proofs and Types","author":"J-Y Girard","year":"1989","unstructured":"Girard, J.-Y., Y. Lafont, and P. Taylor. Proofs and Types, Cambridge University Press, 1989."},{"key":"10101_CR15","doi-asserted-by":"crossref","unstructured":"Girard, J. Y., Une Extension de l\u2019Interpretation de G\u00f6del \u00e0 l\u2019Analyse, et son Application\u00e0 l\u2019\u00c9limination des Coupures dans l\u2019Analyse et la Th\u00e9orie des Types, in J.E. Fenstad, (ed.), Proceedings of the Second Scandinavian Logic Symposium, North-Holland, Amsterdam, 1971, pp. 63\u201392.","DOI":"10.1016\/S0049-237X(08)70843-7"},{"key":"10101_CR16","doi-asserted-by":"crossref","unstructured":"Goldfarb, W., On Dummett\u2019s \u201cproof-theoretic justifications of logical laws\u201d, in T. Piecha, and P. Schroeder-Heister, (eds.), Advances in Proof-theoretic Semantics, vol. 43 of Trends in Logic, Springer, 2016, pp. 195\u2013210.","DOI":"10.1007\/978-3-319-22686-6_13"},{"key":"10101_CR17","unstructured":"Jacobs, B.P.F., Categorical Logic and Type Theory, vol. 141 of Studies in logic and the foundations of mathematics, North-Holland, 2001."},{"key":"10101_CR18","unstructured":"Johnstone, P.T., Stone Spaces, vol. 3 of Cambridge Studies in Advanced Mathematics, Cambridge University Press, 1982."},{"key":"10101_CR19","doi-asserted-by":"crossref","unstructured":"Kripke, S.A., Semantical Analysis of Intuitionistic Logic I, in J.N. Crossley, and M.A.E. Dummett, (eds.), Formal Systems and Recursive Functions, vol. 40 of Studies in Logic and the Foundations of Mathematics, Elsevier, 1965, pp. 92\u2013130.","DOI":"10.1016\/S0049-237X(08)71685-9"},{"key":"10101_CR20","volume-title":"Introduction to Higher Order Categorical Logic","author":"J Lambek","year":"1986","unstructured":"Lambek, J., and P. Scott,Introduction to higher order categorical logic, Cambridge University Press, 1986."},{"key":"10101_CR21","volume-title":"Sheaves in Geometry and Logic: A First Introduction to Topos Theory","author":"Saunders Mac Lane","year":"1992","unstructured":"Mac Lane, S., and I. Moerdijk, Sheaves in Geometry and Logic: A First Introduction to Topos Theory, Springer-Verlag, 1992."},{"key":"10101_CR22","volume-title":"Structural Proof Theory","author":"S Negri","year":"2008","unstructured":"Negri, S., and J. Von Plato, Structural Proof Theory, Cambridge University Press, Cambridge 2008."},{"key":"10101_CR23","doi-asserted-by":"crossref","unstructured":"Piecha, T., Completeness in proof-theoretic semantics, in T. Piecha, and P. Schroeder-Heister, (eds.), Advances in Proof-Theoretic Semantics, vol. 43 of Trends in Logic, Springer, 2016, pp. 231\u2013251.","DOI":"10.1007\/978-3-319-22686-6_15"},{"issue":"3","key":"10101_CR24","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/s10992-014-9322-x","volume":"44","author":"T Piecha","year":"2015","unstructured":"Piecha, T., W. de Campos Sanz, and P. Schroeder-Heister, Failure of Completeness in Proof-theoretic Semantics, Journal of Philosophical Logic 44(3):321\u2013335, 2015.","journal-title":"Journal of Philosophical Logic"},{"issue":"1","key":"10101_CR25","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/s11225-018-9823-7","volume":"107","author":"Thomas Piecha","year":"2019","unstructured":"Piecha, T., and P. Schroeder-Heister, Incompleteness of intuitionistic propositional logic with respect to proof-theoretic semantics, Studia Logica 107(1):233\u2013246, 2019.","journal-title":"Stud Logica"},{"key":"10101_CR26","doi-asserted-by":"crossref","unstructured":"Pistone, P., L. Tranchini, and M. Petrolo, The naturality of natural deduction (II). On atomic polymorphism and generalized propositional connectives, Studia Logica 110:545\u2013592,2022.","DOI":"10.1007\/s11225-021-09964-z"},{"key":"10101_CR27","volume-title":"Natural Deduction: A Proof-Theoretical Study","author":"Dag Prawitz","year":"1965","unstructured":"Prawitz, D., Natural Deduction: A Proof-Theoretical Study, Dover Publications, 1965."},{"key":"10101_CR28","unstructured":"Pym, D.J., E. Ritter, and E. Robinson, Proof-theoretic Semantics in Sheaves (Extended Abstract), in Proceedings of the Eleventh Scandinavian Logic Symposium \u2014 SLSS 11, 2022, pp. 36\u201338."},{"issue":"3","key":"10101_CR29","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/BF01019459","volume":"6","author":"John C Reynolds","year":"1993","unstructured":"Reynolds, J.C., The discoveries of continuations, Lisp and Symbolic Computation, 6(3):233\u2013247, 1993.","journal-title":"Lisp and Symbolic Computation"},{"issue":"5","key":"10101_CR30","doi-asserted-by":"publisher","first-page":"777","DOI":"10.1093\/logcom\/13.5.777","volume":"13","author":"EP Robinson","year":"2003","unstructured":"Robinson, E.P., Proof nets for classical logic, Journal of Logic and Computation 13(5):777\u2013797, 2003.","journal-title":"Journal of Logic and Computation"},{"key":"10101_CR31","unstructured":"Sandqvist, T., A note on definability of logical operators in second-order logic, 2008."},{"key":"10101_CR32","doi-asserted-by":"crossref","unstructured":"Sandqvist, T., Base-extension Semantics for Intuitionistic Sentential Logic, Logic Journal of the IGPL 23(5):719\u2013731, 2015.","DOI":"10.1093\/jigpal\/jzv021"},{"issue":"3","key":"10101_CR33","doi-asserted-by":"publisher","first-page":"525","DOI":"10.1007\/s11229-004-6296-1","volume":"148","author":"P Schroeder-Heister","year":"2006","unstructured":"Schroeder-Heister, P., Validity concepts in proof-theoretic semantics, Synthese 148(3):525\u2013571, 2006.","journal-title":"Synthese"},{"key":"10101_CR34","unstructured":"Schroeder-Heister, P., Proof-Theoretic versus Model-Theoretic \u00a0Consequence, in M. Peli\u0161, (ed.), The Logica Yearbook 2007, FILOSOFIA, Prague, 2008."},{"key":"10101_CR35","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1002\/malq.19830291005","volume":"29","author":"R Seely","year":"1983","unstructured":"Seely, R., Hyperdoctines and natural deduction, Zeitschrift f\u00fcr Mathematische Logik und Grundlagen der Mathematik 29:505\u2013542, 1983.","journal-title":"Zeitschr. f. math Kogik un Grundlagen d. Math"},{"key":"10101_CR36","first-page":"07","volume":"100","author":"W Stafford","year":"2023","unstructured":"Stafford, W., and Nascimento, V., Following all the rules: intuitionistic completeness for generalized proof-theoretic validity, Analysis 100, 07 2023.","journal-title":"Analysis"},{"key":"10101_CR37","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1093\/aristotelian\/79.1.167","volume":"79","author":"N Tennant","year":"1978","unstructured":"Tennant, N., Entailment and Proofs, Proceedings of the Aristotelian Society 79:167\u2013189, 1978.","journal-title":"Proceedings of the Aristotelian Society"},{"key":"10101_CR38","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780198777892.001.0001","volume-title":"Core Logic","author":"N Tennant","year":"2017","unstructured":"Tennant, N., Core Logic, Oxford University Press, Oxford 2017."},{"key":"10101_CR39","unstructured":"Troelstra, A.S., and H. Schwichtenberg, Basic Proof Theory, vol. 43 of Cambridge Tracts in Theoretical Computer Science, 2nd ed., Cambridge University Press, Cambridge, 2000."}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-024-10101-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11225-024-10101-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-024-10101-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,31]],"date-time":"2025-01-31T13:45:14Z","timestamp":1738331114000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11225-024-10101-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,3]]},"references-count":39,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,2]]}},"alternative-id":["10101"],"URL":"https:\/\/doi.org\/10.1007\/s11225-024-10101-9","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"value":"0039-3215","type":"print"},{"value":"1572-8730","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,5,3]]},"assertion":[{"value":"6 March 2023","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 May 2024","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}