 However, this similarity in the logical behavior of (10) and (11) should not obscure the great differences between the biconditional (‘\(\leftrightarrow\)’) and definitional equivalence (‘\(\eqdf\)’). The former is a sentential connective, but the latter is trans-categorical: not only formulas, but also predicates, names, and items of other logical categories can occur on the two sides of ‘\(\eqdf\)’. Moreover, the biconditional can be iterated—e.g., \(((\phi \leftrightarrow \psi) \leftrightarrow \chi)\)—but not definitional equivalence. Finally, a term can be introduced by a stipulative definition into a ground language whose logical resources are confined, say, to classical conjunction and disjunction. This is perfectly feasible, even though the biconditional is not expressible in the language. In such cases, the inferential role of the stipulative definition is not mirrored by any formula of the extended language.