On the equivalence of proofs involving identity
type: Item
instance of: scholarly article
title: On the equivalence of proofs involving identity
zbMATH Open document ID: 0653.03037
author: Glen Helman
published in: Notre Dame Journal of Formal Logic
publication date: 1987-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03G30
zbMATH DE Number: 4064985
zbMATH Keywords: natural deduction proofs
zbMATH Keywords: first-order logic with identity
zbMATH Keywords: normalization
zbMATH Keywords: applications of category-theory to proofs
zbMATH Keywords: proof-equivalence
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1305/ndjfl/1093637554
OpenAlex ID: W2084576343
DOI: 10.1305/NDJFL/1093637554
description: scientific article; zbMATH DE number 4064985