On the equivalence of proofs involving identity (Q1107527)

In the following, we will consider relations of equivalence defined on natural deduction proofs for first-order logic with identity. Such equivalence relations can be derived from theories of normalization, and they are imposed in applications of category-theory to proofs. Our main concern here will be with principles of proof-equivalence for various choices of identity rules. Independent treatments of identity are not common either in accounts of normalization or in the relevant work in category-theory, and we will approach proof-equivalence directly, with only passing comments on its connection with these two fields. The discussion will center on two topics. First, we will develop a pair of moderately strong relations for each of the two usual sets of rules for identity, rules characterizing it as a congruence and as supporting replacement in all contexts. We will also consider two sets of rules for identity that are more analogous to the introduction and elimination rules employed for other constants. Each of these sets of rules suggests principles of proof-equivalence, but the resulting relations prove to be different from those developed for the congruence and replacement rules and are in some ways less satisfactory.