I take some initial steps toward a theory of real deﬁnition, drawing upon recent developments in higher-order logic. The resulting account allows for extremely ﬁne- grained distinctions (i.e., it can distinguish between any relata that diﬀer in their syntactic structure, while avoiding the Russell-Myhill problem). It is the ﬁrst account that can consistently embrace three desirable logical principles that initially appear to be incompatible: the Identiﬁcation Hypothesis (if F is, by deﬁnition, G then F is the same as G), Irreﬂexivity (...) (there are no reﬂexive deﬁnitions) and Leibniz’s Law. Additionally, it possesses the resources to resolve the paradox of analysis. (shrink)