AbstractThe concept of direct computation used by Statman (1977) was instrumental in the development of a notion of normal form for proofs of equality. In order to find a functional (Curry–Howard style) interpretation of direct computations we take a closer look at proof procedures for first-order sentences with equality drawing the attention to the need for introducing (function) symbols for rewrites. This leads us to a proposal to the effect that the framework of labelled natural deduction gives the right tools to formulate a proof theory for the “logical connective” of propositional equality in the style of the so-called Curry–Howard interpretation. The basic idea is that when analysing an equality sentence into (i) proof conditions (introduction) and (ii) immediate consequences (elimination), it becomes clear that we need to bring in identifiers (i.e. function symbols) for sequences of rewrites, and this is what we claim is the missing entity in P. Martin-Löfʼs equality types (both intensional and extensional). For the proof system for equality we establish a normalisation procedure, proving that it is terminating and confluent.11Part of this material was presented in June 2006 at the Logical Methods in the Humanities Seminar, Stanford University, and the authors would like to thank Solomon Feferman and Grigori Mints for their comments and suggestions. The main results were produced while the first author was Edward Larocque Tinker Visiting Professor at the Department of Philosophy, Stanford Univ, and the second author was a Visiting Scholar at CSLI, Stanford.