 The third idea—reduction—is that the use of a formula \(Z\) containing the defined term is explained by reducing \(Z\) to a formula in the ground language. This idea, when conjoined with the primacy of the sentential, leads to a strong version of the Use criterion, called the Eliminability criterion: the definition must reduce each formula containing the defined term to a formula in the ground language, i.e., one free of the defined term. Eliminability is the distinctive thesis of the traditional account and, as we shall see below, it can be challenged.