*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.

I’m *Greg Restall*, and this is my personal website. ¶ I am the Shelby Cullom Davis Professor of Philosophy at the University of St Andrews.

- greg@consequently.org
- keybase.io/consequently, to sign or encrypt a message to send to me privately.
- @consequently on Twitter.
- @consequently on Instagram.
- @consequently on GitHub.

To receive updates from this site, you can subscribe to the RSS feed of all updates to the site in an RSS feed reader, or follow me on Twitter at @consequently, where I’ll update you if anything is posted.