A proof-theoretic treatment of definite descriptions 'the F' that need not pick out a unique F. It replaces the identity in Russell's uniqueness clause with qualified identity ('a and b agree in all Q-respects', where Q is a chosen set of predicates), yielding graded notions of qualified uniqueness and definiteness: strict when Q is all predicates, and restricted (loose) when Q is a proper subset. The account is formalized in an intuitionistic bipredicational natural-deduction system with normalization and the subformula property, and interpreted by a proof-theoretic rather than model-theoretic semantics.
A proof-theoretic account of 'incomplete' definite descriptions, i.e. uses of 'the F' where more than one F exists. On Russell's analysis, 'the F is G' asserts existence, uniqueness, and predication,…