Abstract
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’s (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’s constructions. This naturality includes Sandqvist’s 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’s semantics can also be viewed as the natural disjunction in a category of sheaves.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Bellin, G., H. Martin, and P. Edmund, Robinson, and Christian Urban Categorical proof theory of classical propositional calculus, Theoretical Computer Science, 364:146–165, 2006.
Blackburn, P., M. de Rijke, and Y. Venema, Modal Logic, Cambridge University Press, 2001.
van Dalen, D., Logic and Structure, Springer, Cham, 5th edition, 2012.
Dummett, M., The Logical Basis of Metaphysics, Harvard University Press, 1993.
Espirito Santo, J., and G. Ferreira, A refined interpretation of intuitionistic logic by means of atomic polymorphism, Studia Logica 108:477–507, 2020.
Ferreira, F., Comments on predicative logic, Journal of Philosophical Logic 35(1):1–8, 2006.
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, Łódź University Press, Lódź, 2014, pp. 55–65.
Ferreira, F., and G. Ferreira, Atomic polymorphism. The Journal of Symbolic Logic 78(1):260–274, 2013.
Ferreira, F., and G. Ferreira, The faithfulness of fat: a proof-theoretic proof, Studia Logica 103(6): 1301, 2015.
Führmann, C., and D. Pym, Order-enriched categorical models of the classical sequent calculus, Journal of Pure and Applied Algebra 204(1):21–78, 2006.
Gentzen, G., Untersuchungen Über Das Logische Schließen. II. Mathematische Zeitschrift 39:405–431, 1935.
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.
Girard, J.Y., Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. Thèse de Doctorat d’Etat, Université Paris VII, 1972.
Girard, J.-Y., Y. Lafont, and P. Taylor. Proofs and Types, Cambridge University Press, 1989.
Girard, J. Y., Une Extension de l’Interpretation de Gödel à l’Analyse, et son Applicationà l’Élimination des Coupures dans l’Analyse et la Théorie des Types, in J.E. Fenstad, (ed.), Proceedings of the Second Scandinavian Logic Symposium, North-Holland, Amsterdam, 1971, pp. 63–92.
Goldfarb, W., On Dummett’s “proof-theoretic justifications of logical laws”, in T. Piecha, and P. Schroeder-Heister, (eds.), Advances in Proof-theoretic Semantics, vol. 43 of Trends in Logic, Springer, 2016, pp. 195–210.
Jacobs, B.P.F., Categorical Logic and Type Theory, vol. 141 of Studies in logic and the foundations of mathematics, North-Holland, 2001.
Johnstone, P.T., Stone Spaces, vol. 3 of Cambridge Studies in Advanced Mathematics, Cambridge University Press, 1982.
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–130.
Lambek, J., and P. Scott,Introduction to higher order categorical logic, Cambridge University Press, 1986.
Mac Lane, S., and I. Moerdijk, Sheaves in Geometry and Logic: A First Introduction to Topos Theory, Springer-Verlag, 1992.
Negri, S., and J. Von Plato, Structural Proof Theory, Cambridge University Press, Cambridge 2008.
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–251.
Piecha, T., W. de Campos Sanz, and P. Schroeder-Heister, Failure of Completeness in Proof-theoretic Semantics, Journal of Philosophical Logic 44(3):321–335, 2015.
Piecha, T., and P. Schroeder-Heister, Incompleteness of intuitionistic propositional logic with respect to proof-theoretic semantics, Studia Logica 107(1):233–246, 2019.
Pistone, P., L. Tranchini, and M. Petrolo, The naturality of natural deduction (II). On atomic polymorphism and generalized propositional connectives, Studia Logica 110:545–592,2022.
Prawitz, D., Natural Deduction: A Proof-Theoretical Study, Dover Publications, 1965.
Pym, D.J., E. Ritter, and E. Robinson, Proof-theoretic Semantics in Sheaves (Extended Abstract), in Proceedings of the Eleventh Scandinavian Logic Symposium — SLSS 11, 2022, pp. 36–38.
Reynolds, J.C., The discoveries of continuations, Lisp and Symbolic Computation, 6(3):233–247, 1993.
Robinson, E.P., Proof nets for classical logic, Journal of Logic and Computation 13(5):777–797, 2003.
Sandqvist, T., A note on definability of logical operators in second-order logic, 2008.
Sandqvist, T., Base-extension Semantics for Intuitionistic Sentential Logic, Logic Journal of the IGPL 23(5):719–731, 2015.
Schroeder-Heister, P., Validity concepts in proof-theoretic semantics, Synthese 148(3):525–571, 2006.
Schroeder-Heister, P., Proof-Theoretic versus Model-Theoretic Consequence, in M. Peliš, (ed.), The Logica Yearbook 2007, FILOSOFIA, Prague, 2008.
Seely, R., Hyperdoctines and natural deduction, Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 29:505–542, 1983.
Stafford, W., and Nascimento, V., Following all the rules: intuitionistic completeness for generalized proof-theoretic validity, Analysis 100, 07 2023.
Tennant, N., Entailment and Proofs, Proceedings of the Aristotelian Society 79:167–189, 1978.
Tennant, N., Core Logic, Oxford University Press, Oxford 2017.
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.
Acknowledgements
We are grateful to the anonymous reviewers and to Alexander Gheorghiu and Tao Gu for helpful comments on this work.
Author information
Authors and Affiliations
Corresponding authors
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Presented by Heinrich Wansing.
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
About this article
Cite this article
Pym, D., Ritter, E. & Robinson, E. Categorical Proof-theoretic Semantics. Stud Logica (2024). https://doi.org/10.1007/s11225-024-10101-9
Received:
Published:
DOI: https://doi.org/10.1007/s11225-024-10101-9