What are acceptable reductions?

Perspectives from proof-theoretic semantics and type theory

Abstract

It has been argued that reduction procedures are closely connected to the question about identity of proofs and that accepting certain reductions would lead to a trivialization of identity of proofs in the sense that every derivation of the same conclusion would have to be identifed. In this paper it will be shown that the question, which reductions we accept in our system, is not only important if we see them as generating a theory of proof identity but is also decisive for the more general question whether a proof has meaningful content. There are certain reductions which not only would force us to identify proofs of different arbitrary formulas but which would render derivations in a system allowing them meaningless.