 That is, any formula of \(L\) that is provable using definition \(\mathcal{D}\) is also provable without using \(\mathcal{D}\): the definition does not enable us to prove anything new in \(L\). The Eliminability criterion can be made precise thus: