 An especially significant case in which this reasoning can be applied is the case of standard Fregean first-order quantificational languages, under a wide array of pretheoretic conceptions of logical truth. It is typical to accept that all formulae derivable in a typical first-order calculus are universally valid, true in all counterfactual circumstances, a priori and analytic if any formula  is.[10]  So (4) holds under a wide array of pretheoretic conceptions in this case. (6) holds too for the typical calculi in question, in virtue of Gödel's completeness theorem, so (5) holds. This means that one can convince oneself that both derivability and model-theoretic validity are extensionally correct characterizations of our favorite pretheoretic notion of logical truth for first-order languages, if our pretheoretic conception is not too eccentric. The situation is not so clear in other languages of special importance for the Fregean tradition, the higher-order quantificational languages.