Identity of Proofs

Proof-theoretic semantics is here presented as primarily concerned with the investigation of the relationship between proofs (understood as abstract entities) and derivations (the linguistic representations of proofs). This relationship is taken to be analogous to that between names and (abstract) objects in Frege. On this conception of proof-theoretic semantics, reductions and expansions should be viewed as identity-preserving operations on derivations and thus as inducing an equivalence relation on derivations such that equivalent derivations denote the same proof. Using this equivalence on derivations it is possible to define an equivalence relation on formulas that is stricter than interderivability, called isomorphism. We argue that identity of proofs and formula isomorphism show the intensional nature of this conception of proof-theoretic semantics. Finally, this conception is compared to the one advocated by Dummett and Prawitz, which is based on a notion of validity of derivations.