 It follows from Gödel's first incompleteness theorem that already for a second-order language there is no calculus \(C\) where derivability is sound with respect to model-theoretic validity and which makes true (6) (for the notion of model-theoretic validity as usually defined for such a language). We may call this result the incompleteness of second-order calculi with respect to model-theoretic validity. Said another way: for every second-order calculus \(C\) sound with respect to model-theoretic validity there will be a formula \(F\) such that \(\text{MTValid}(F)\) but it is not the case that \(\text{DC}(F)\).