Descriptions in mathematical logic

Abstract

After a discussion of the different treatments in the literature of vacuous descriptions, the notion of descriptor is slightly generalized to function descriptor , so as to form partial functions which satisfy $\forall \overset{\lower0.5em\hbox{$\smash{\scriptscriptstyle\rightharpoonup}$}} {x} z\left( {z = \varphi \overset{\lower0.5em\hbox{$\smash{\scriptscriptstyle\rightharpoonup}$}} {x} \leftrightarrow \forall y\left( {A\left( {\overset{\lower0.5em\hbox{$\smash{\scriptscriptstyle\rightharpoonup}$}} {x} ,y} \right) \leftrightarrow y = z} \right)} \right)$. We use (intuitionistic, classical or intermediate) logic with existence predicate, as introduced by D. S. Scott, 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.