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 identified. 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 would not only force us to identify proofs of different arbitrary formulas but which would render derivations in a system allowing them meaningless. To exclude such cases, a minimal criterion is proposed which reductions have to fulfill to be acceptable.

翻译：已有论证表明，归约程序与证明同一性问题密切相关，且若接受某些归约，将导致证明同一性被琐碎化——即所有导出相同结论的推导都必须被视为等同。本文旨在揭示：我们系统中所接受的归约类型，不仅关乎其能否生成证明同一性理论，更决定了证明是否具有有意义内容这一根本性问题。存在某些归约，它们不仅会强制我们认同不同任意公式的证明，更会使允许此类归约的系统中的推导失去意义。为排除此类情形，本文提出一个归约需满足的最低限度的可接受性标准。