  (The proof that Tarski seems to have in mind is this: suppose that X is a Tarskian logical consequence of K; then there is no model of K which is not a model of X; so there is no substitution instance &lt;K′, X′&gt; of &lt;K, X&gt; such that the sentences in K′ are true and X′ is false; for if there was one such, it would readily provide an interpretation—constituted by the extensions of the extra-logical constants of &lt;K′, X′&gt;—which would constitute a model of K that would not be a model of X. But whether this is the proof Tarski had in mind is a disputed exegetical question.)