Russell’s theory of definite descriptions in the light of structural proof-theory

In ‘On Denoting’ Russell proposed the most influential theory of definite descriptions, expressions of the form ‘the F ’. Characteristic for Russell’s approach is that definite descriptions are not treated as what they appear to be on the surface, i.e. as singular terms. Instead they are eliminated by a contextual definition. Russell formalises definite descriptions in the context of complete sentences of the form ‘The F is G ’. This requires scope markers to distinguish, e.g., internal from external negation. It was recognised by Burge, and Kalish and Montague, however, that the essential features of Russell’s approach may be formalised while respecting the syntactic category to which definite descriptions appear to belong. An alternative, favoured by Neale, follows Russell in that complete sentences ‘The F is G ’ are formalised by a binary quantifier. The undeniable importance of the theory of definite descriptions for logic, mathematics and philosophy demands that it be formalised to meet the standards of modern proof theory. This is the topic of the present paper. We systematise, compare and extend existing approaches. After presenting its essential features, we formalise Russell’s theory of definite descriptions in sequent calculus. Three approaches will be considered. The first uses a binary quantifier, whereas the remaining two employ the term-forming iota operator. The first of these employs only the iota operator, the other employs in addition the lambda operator which does duty as a scope marker. All systems satisfy the standards for modern proof theory, in particular cut elimination. The appendix reformulates these systems in natural deduction, which is more convenient for practical purposes.