 (If \(F\) is a formula of a first-order language without identity, then if no replacement instance of the form of \(F\) is false, this is a sufficient condition for \(F\)'s being model-theoretically valid. As it turns out, if \(F\) is not model-theoretically valid, then some replacement instance of its form whose variables range over the natural numbers and whose non-logical constants are arithmetical expressions will be false. This can be justified by means of a refinement of the Löwenheim-Skolem theorem. See the entry on  logic, classical,  and Quine 1970, ch. 4, for discussion and references. No similar results hold for higher-order languages.)