In this note we present a sound, complete, and cut-free tableau calculus for the logic being a formalisation of a Russell-style theory of DD with the iota-operator used to construct DD, the lambda-operator forming predicate-abstracts, and DD as genuine terms with a restricted right of residence. We show that in this setting we are able to overcome problems typical for 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 DD-counterpart under a given theory.