A central problem in proof-theory is that of finding criteria for identity of proofs, that is, for when two distinct formal derivations can be taken as denoting the same logical argument. In the literature one finds criteria which are either based on proof normalization (two derivations denote the same proofs when they have the same normal form) or on the association of formal derivations with graph-theoretic structures (two derivations denote they same proof when they are associated with the same graph). In this paper we argue for a new criterion for identity of proofs which arises from the interpretation of formal rules and derivations as natural transformations of a suitable kind. We show that the naturality conditions arising from this interpretation capture in a uniform and elegant ways several forms of "rule-permutations" which are found in proof-systems for propositional, first- and second-order logic.
翻译:证据理论的一个中心问题是找到证据身份的标准,也就是说,在两种不同的正式推断可被看作指同一种逻辑论点。在文献中,人们发现的标准要么是基于证据正常化(两种推断指同一种正常形式时的相同证明),要么是基于正式推断与图形理论结构的联系(两种推断指同一种图表相关时的相同证据)。在本文中,我们主张对正式规则的解释所产生的证据身份的新标准以及衍生物作为适当类型的自然变换。我们表明,这种解释以统一和优雅的方式捕捉了几种“规则差异”的自然条件,这些形式在假设、第一和第二顺序逻辑的举证制度中是存在的。