What is the Meaning of Proofs?
Tóm tắt
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.
Tài liệu tham khảo
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.