Abstract
The origins of proof-theoretic semantics lie in the question of what constitutes the meaning of the logical connectives and its response: the rules of inference that govern the use of the connective. However, what if we go a step further and ask about the meaning of a proof as a whole? In this paper we address this question and lay out a framework to distinguish sense and denotation of proofs. Two questions are central here. First of all, if we have two (syntactically) different derivations, does this always lead to a difference, firstly, in sense, and secondly, in denotation? The other question is about the relation between different kinds of proof systems (here: natural deduction vs. sequent calculi) with respect to this distinction. Do the different forms of representing a proof necessarily correspond to a difference in how the inferential steps are given? In our framework it will be possible to identify denotation as well as sense of proofs not only within one proof system but also between different kinds of proof systems. Thus, we give an account to distinguish a mere syntactic divergence from a divergence in meaning and a divergence in meaning from a divergence of proof objects analogous to Frege’s distinction for singular terms and sentences.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Barendregt, H., & Ghilezan, S. (2000). Lambda terms for natural deduction, sequent calculus and cut elimination. Journal of Functional Programming, 10(1), 121–134.
De Groote, P. (1999). On the strong normalisation of natural deduction with permutation-conversions. In Narendran, P., & Rusinowitch, M. (Eds.) Rewriting Techniques and Applications: RTA 1999 (pp. 45–59). Berlin/Heidelberg: Springer.
Došen, K. (2003). Identity of proofs based on normalization and generality. Bulletin of Symbolic Logic, 9, 477–503.
Došen, K. (2008). Cut Elimination in Categories. Berlin: Springer.
Dummett, M. (1973). Frege: Philosophy of language. New York: Harper & Row.
Duží, M., Jespersen, B., & Materna, P. (2010). Procedural semantics for hyperintensional logic: Foundations and applications of transparent intensional logic. Berlin: Springer.
Francez, N. (2017). On harmony and permuting conversions. Journal of Applied Logic, 21, 14–23.
Frege, G. (1948[1892]). Sense and reference. The Philosophical Review, 57(3), 209–230.
Frege, G. (1979). Posthumous writings. Oxford: Basil Blackwell.
Friedman, H. (1975). Equality between functionals. In Parikh, R. (Ed.) Logic colloquium: Lecture notes in mathematics, (Vol. 453 pp. 23–37). Berlin/Heidelberg: Springer.
Girard, J.-Y. (1989). Proofs and types. Cambridge: Cambridge University Press.
Hacking, I. (1979). What is Logic? The Journal of Philosophy, 76(6), 285–319.
Herbelin, H. (1994). A lambda-calculus structure isomorphic to Gentzen-style sequent calculus structure. Computer Science Logic, 61–75.
Kreisel, G. (1971). A survey of proof theory II. In Fenstad, J.E. (Ed.) Proceedings of the second Scandinavian logic symposium (pp. 109–170). Amsterdam: North-Holland.
Lindley, S. (2007). Extensional rewriting with sums. In Ronchi Della Rocca, S. (Ed.) Typed Lambda Calculi and Applications: TLCA 2007 (pp. 255–271). Berlin/Heidelberg: Springer.
Martin-Löf, P. (1975). About models for intuitionistic type theories and the notion of definitional equality. In Kanger, S. (Ed.) Proceedings of the third Scandinavian logic symposium (pp. 81–109). Amsterdam: North-Holland.
Muskens, R. (2005). Sense and the computation of reference. Linguistics and Philosophy, 28(4), 473–504.
Negri, S., & von Plato, J. (2001). Structural proof theory. Cambridge/New York: Cambridge University Press.
Pfenning, F. (2000). Structural cut elimination: I. Intuitionistic and classical logic. Information and Computation, 157, 84–141.
Pottinger, G. (1977). Normalization as a homomorphic image of cut-elimination. Annals of Mathematical Logic, 12, 323–357.
Prawitz, D. (1965). Natural deduction. Stockholm: Almqvist & Wiksell.
Prawitz, D. (1971). Ideas and results in proof theory. In Fenstad, J.E. (Ed.) Proceedings of the second Scandinavian logic symposium (pp. 235–307). Amsterdam: North-Holland.
Sørensen, M., & Urzyczyn, P. (2006). Lectures on the Curry-Howard isomorphism. Amsterdam: Elsevier Science.
Statman, R. (1983). λ-definable functionals and βη conversion. Archiv für Mathematische Logik, 23, 21–26.
Sundholm, G. (1994). Proof-Theoretical Semantics and Fregean identity criteria for propositions. The Monist, 77(3), 294–314.
Tranchini, L. (2016). Proof-theoretic semantics, paradoxes and the distinction between sense and denotation. Journal of Logic and Computation, 26 (2), 495–512.
Tranchini, L. (2018). Stabilizing quantum disjunction. Journal of Philosophical Logic, 47, 1029–1047.
Troelstra, A., & Schwichtenberg, H. (2000). Basic proof theory, 2nd edn. Cambridge: Cambridge University Press.
Urban, C. (2014). Revisiting Zucker’s work on the correspondence between cut-elimination and normalisation. In Pereira, L., Haeusler, E., & de Paiva, V. (Eds.) Advances in natural deduction: A celebration of Dag Prawitz’s work (pp. 31–50). Dordrecht: Springer.
Widebäck, F. (2001). Identity of proofs. Stockholm: Almquist & Wiksell International.
Zucker, J. (1974). The correspondence between cut-elimination and normalization. Annals of Mathematical Logic, 7, 1–112.
Funding
Open Access funding enabled and organized by Projekt DEAL.
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher’s Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
I would like to thank several people for supporting me in improving this paper essentially, among them Luca Tranchini for his thorough feedback and vital input on an earlier version of this paper and also two anonymous referees for their very constructive and helpful reports. I am especially grateful to Heinrich Wansing for the numerous and encouraging occasions to discuss this paper extensively and for his valuable comments.
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
Ayhan, S. What is the Meaning of Proofs?. J Philos Logic 50, 571–591 (2021). https://doi.org/10.1007/s10992-020-09577-2
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10992-020-09577-2