Comparing Rules for Identity in sequent systems and natural deduction

September 6, 2021

Abstract: It is straightforward to treat the identity predicate in models for first order predicate logic. Truth conditions for identity formulas are given by a natural clause: a formula s = t is true (or satisfied by a variable assignment) in a model if and only if the denotations of the terms s and t (perhaps relative to the given variable assignment) are the same.

On the other hand, finding appropriate rules for identity in a sequent system or in a natural deduction proof setting leaves a number of questions open. Identity could be treated with introduction and elimination rules in natural deduction, or left and right rules, in a sequent calculus, as is standard for familiar logical concepts. On the other hand, since identity is a predicate and identity formulas are atomic, it is also very natural to treat identity by way of axiomatic sequents, rather than by inference rules. I will describe and discuss this phenomenon, and explore the relationships between different formulations of rules for the identity predicate, and attempt to account for some of the distinctive virtues of each different formulation.

• The talk is an invited online presentation for the Tableaux 2021.

• The slides for the talk are available here.