What is the meaning of proofs? A Fregean distinction in proof-theoretic semantics

TL;DR

This paper explores the meaning of proofs in proof-theoretic semantics by distinguishing sense and denotation, comparing different proof systems, and providing a framework to analyze their semantic differences.

Contribution

It introduces a novel framework to differentiate sense and denotation of proofs across various proof systems, extending Fregean distinctions to proof-theoretic semantics.

Findings

Framework distinguishes sense and denotation of proofs

Identifies semantic differences between proof systems

Allows comparison of proof objects across systems

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.