What is the Meaning of Proofs?
- PDF / 393,686 Bytes
- 21 Pages / 439.642 x 666.49 pts Page_size
- 104 Downloads / 215 Views
What is the Meaning of Proofs? A Fregean Distinction in Proof-Theoretic Semantics Sara Ayhan1 Received: 2 November 2019 / Accepted: 14 September 2020 / © The Author(s) 2020
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. Keywords Proof-theoretic semantics · Sense · Denotation · Identity of proofs
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. Sara Ayhan
[email protected] 1
Institute of Philosophy I, Ruhr University Bochum, Bochum, Germany
S. Ayhan
1 Introduction In proof-theoretic semantics (PTS) the meaning of the logical constants is taken to be given by the rules of inference that govern their use. As a proof is constituted by applications of rules of inference, it seems reasonable to ask what the meaning of proofs as a whole would consist of on this account. What we are particularly interested in is a Fregean distinction between sense and denotation in the context of proofs.1 This account builds up on [26], where such a distinction is proposed and used in a proof-theoretic explanation of paradoxes. The notion of denotation is nothing new in the context of proofs. It is common in the literature on proof theory and PTS (e.g. [14, p. 6], [16, 22]) to distinguish between derivations, as linguistic objects, and proofs, as abstract (in the intuitionistic tradition: mental) entities. Proofs are then said to be represented or denoted by derivations, i.e. the abstract proof object is the denotation of a derivation. The notion of
Data Loading...
