 Let us now see how Conservativeness and Eliminability can be made precise. First consider languages that have a precise proof system of the familiar sort. Let the ground language \(L\) be one such. The proof system of \(L\) may be classical, or three-valued, or modal, or relevant, or some other; and it may or may not contain some non-logical axioms. All we assume is that we have available the notions “theorem of \(L\)” and “provably equivalent in \(L\),” and also the notions “theorem of \(L^{+}\)” and “provably equivalent in \(L^{+}\)” that result when the proof system of \(L\) is supplemented with a definition \(\mathcal{D}\) and the logical rules governing definitions. Now, the Conservativeness criterion can be made precise as follows.