 In general, there are no fully satisfactory philosophical arguments for the thesis that model-theoretic validity is unsound with respect to logical truth in higher-order languages. Are there then any good reasons to think that derivability (in any calculus sound for model-theoretic validity) must be incomplete with respect to logical truth? There don't seem to be any absolutely convincing reasons for this view either. The main argument (the first version of which was perhaps first made explicit in Tarski 1936a, 1936b) seems to be this. As noted above, Gödel's first incompleteness theorem implies that for any calculus for a higher-order language there will be a model-theoretically valid formula that will not be derivable in the calculus. As it turns out, the formula obtained by the Gödel construction is also always intuitively true in all domains (set-theoretical or not), and it's reasonable to think of it as universally valid. (It's certainly not a formula false in a proper class structure.) The argument concludes that for any calculus there are logically true formulae that are not derivable in it.