Descriptions in Mathematical Logic

After a discussion of the different treatments in the literature of vacuous descriptions, the notion of descriptor is slightly generalized to function descriptor Ⅎy→(x), so as to form partial functions φ = Ⅎy→(x).A→(x, y) which satisfy ∀→xz(z = φx→ ↔ ∀y(A(x→, y) ↔ y = z)). We use (intuitionistic, classical or intermediate) logic with existence predicate, as introduced previously, to handle partial functions, and prove that adding function descriptors to a theory based on such a logic is conservative, For theories with quantification over functions, the situation is different: there the addition of Ⅎ yields new theorems in the Ⅎ-free fragment, but an axiomatisation is easily given. The proofs are syntactical