  The idea that introduction and/or elimination rules fix the sense of a logical constant is often motivated by talk of the rules as defining the constant.  Gentzen remarks that the natural deduction rules “represent, as it were, the ‘definitions’ of the symbols concerned, and the eliminations are no more, in the final analysis, than the consequences of these definitions” (1935, §5.13; 1969, 80). However, a genuine definition would permit the constant to be eliminated from every context in which it occurs (see the entry on Definitions), and introduction and elimination rules for logical constants do not, in general, permit this. For example, in an intuitionistic sequent calculus, there is no sequent (or group of sequents) not containing \(\dq{\rightarrow}\) that is equivalent to the sequent \(\dq{A \rightarrow B \vdash C}\). For this reason, Kneale (1956, 257) says only that we can “treat” the rules as definitions, Hacking (1979) speaks of the rules “not as defining but only as characterizing the logical constants,” and Došen (1994) says that the rules provide only an “analysis,” not a  definition.[23]