 For concreteness, let us fix the ground language \(L\) to be a classical first-order language with identity. The proof system of \(L\) may contain some non-logical axioms \(T\); the interpretations of \(L\) are then the classical models of \(T\). As before, \(L^{+}\) is the expanded language that results when a definition \(\mathcal{D}\) of a non-logical constant \(X\) is added to \(L\); hence, \(X\) may be a name, a predicate, or a function-symbol. Call two definitions equivalent iff they yield the same theorems in the expanded language. Then, it can be shown that if \(\mathcal{D}\) meets the criteria of Conservativeness and Eliminability then \(\mathcal{D}\) is equivalent to a definition in normal form as specified  below.[6]  Since definitions in normal form meet the demands of Conservativeness and Eliminability, the traditional account implies that we lose nothing essential if we require definitions to be in normal form.