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.

翻译：证明论语义学的起源在于一个核心问题：逻辑联结词的意义由什么构成？其答案是：支配联结词使用的推理规则。然而，如果我们进一步追问，一个完整的证明本身具有何种意义？本文针对这一问题展开讨论，并提出一个用于区分证明的"涵义"（Sinn）与"所指"（Bedeutung）的理论框架。以下两个问题至关重要。首先，当存在两个（句法上）不同的推导时，这是否必然导致二者在涵义上有所差异？其次，在所指层面是否也是如此？另一个问题涉及不同证明系统（本文具体指自然演绎与矢列演算）在这一区分框架下的关系：表征证明的不同形式是否必然对应于推演步骤呈现方式的差异？在本文提出的框架中，我们不仅能区分单一证明系统内的证明之涵义与所指，还能跨不同证明系统实现这一区分。由此，我们可以将纯粹句法上的分歧与意义层面的分歧，以及意义层面的分歧与证明对象层面的分歧加以区分——这类似于弗雷格对单称词项和句子所作的经典区分。