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.

翻译：在《论指称》中，罗素提出了最具影响力的限定摹状词理论，即形如"那个F"的表达。罗素方法的特征在于，限定摹状词并不按其表面形式被处理为单称词项，而是通过语境定义被消解。罗素在"那个F是G"这类完整句子的语境中形式化限定摹状词，这需要作用域标记来区分内否定与外否定等情形。然而，伯奇、卡利什和蒙塔古指出，罗素方法的基本特征可以在尊重限定摹状词表面所属句法范畴的前提下形式化。而尼尔倾向于另一种方案，他追随罗素，用二元量词形式化"那个F是G"这类完整句子。限定摹状词理论对逻辑学、数学与哲学具有不可否认的重要性，这要求其形式化必须达到现代证明论的标准——这正是本文的研究主题。我们系统化、比较并拓展了现有方法。在呈现其基本特征后，我们采用矢列演算对罗素的限定摹状词理论进行形式化。将考虑三种方案：第一种使用二元量词，其余两种采用生成词项的ι算子——其中一种仅使用ι算子，另一种则额外使用作为作用域标记的λ算子。所有系统均满足现代证明论标准，特别是切割消去性质。附录以更便于实际应用的自然演绎形式重新表述了这些系统。