When iota meets lambda

Definite descriptions are widely discussed in linguistics and formal semantics, but their formal treatment in logic is surprisingly modest. In this article we present a sound, complete, and cut-free tableau calculus TCR lambda for the logic L-R lambda being a formalisation of a Russell-style theory of definite descriptions with the iota-operator used to construct definite descriptions, the lambda-operator forming predicate-abstracts, and definite descriptions as genuine terms with a restricted right of residence. We show that in this setting we are able to overcome problems typical of Russell's original theory, such as scoping difficulties or undesired inconsistencies. We prove the Craig interpolation property for the proposed theory, which, through the Beth definability property, allows us to check whether an individual constant from a signature has a definite description-counterpart under a given theory.