Tableaux Rules for Theories of Definite Descriptions in Positive Free Logic with Some Philosophical Remarks

While Russell's theory of definite descriptions, expressions of the form 'the F', is almost incontrovertible in classical logic, in free logic matters stand differently.Several alternatives have been proposed.In Lambert's hierarchy, the weakest theory is his minimal free theory of definite descriptions (MFD), which only says that anything is the F iff it is the unique existing F, the strongest one is a chosen object theory in which all improper definite descriptions refer to the same object (FD2).Intermediate is Lambert's FD1, which adds ι x(x = t) = t as an axiom to MFD.MFD is very weak.FD2 is very strong.One might hope to find intermediate systems in which ι x(x = t) = t is provable from more fundamental principles.The present paper considers one avenue where one might hope to find them and closes it.Two theories, FDA and FDH, will be considered that are motivated by considerations from proof-theoretic semantics.The former turns out to be equivalent to FD2, the latter to have unreasonable consequences.A third theory, similarly motivated, is also not viable.The philosophical upshot of this is briefly discussed.