At the end of a long process of "rumination" on "old" math log textbooks, I've found the "missing link" - from my personal point of view - between some issues I've raised in the previous months :
(i) the modern definition of valid formula : see this post.
(ii) the "shift" in focus, between the '30s and the '60s, in mathematical logic textbooks, from validity to logical consequence.
Here are some references : in Raymond Smullyan, First Order-Logic (1968 - Dover reprint) and J.L.Bell & A.B.Slomson, Models and Ultraproducts (1969), for example, a definition of "logical consequence" is missing.
In Stephen Cole Kleene, Mathematical Logic (1967 - Dover reprint) there are two different relations of "logical consequence" : the usual one, $\vDash$, and the notation $\phi \vDash^x \psi$, that basically reduces to $(\forall x)\phi \vDash \psi$ in the usual sense.
In Elliott Mendelson, Introduction to Mathematical Logic (4th ed - 1997) the notion of validity is basic, with logical consequence defined in a way that cause some "tricky" details : see this post.
(iii) the original Gödel's proof of his Completeness Theorem and his "modern evolution" (through Henkin's proof) into the model existence lemma (see also this post ).
(iv) and last, the correct explanation (from my point of view) of the link between the names of the famous Gödel's results, that so much give troubles to a lot of students).
What follows is not a question : my hope is that it can be useful to clarify some historical and conceptual issues.
I've found this historical explanation in John Etchemendy, TARSKI ON TRUTH AND LOGICAL CONSEQUENCE, The Journal of Symbolic Logic, Vol_53, 1988, page 75-on.
He discuss the role of Tarski and his
emphasis on logical consequence over logical truth. We find this emphasis in virtually all of Tarski's treatments of these notions.
Thus this characterization [in terms of consequence] of logical truth involves a subtle, and distinctly non-Russellian, contrast between the status of logical and nonlogical axioms: the former must themselves be construed as rules of inference, as part of the mechanism of deduction itself, while the latter are seen as genuine premises or assumptions on which their consequences depend. This distinction is now easily motivated by the semantic account of the logical notions, as well as the various non-axiomatically-based deductive systems later devised by Jaskowski, Gentzen and others. But at the time of these papers [Tarski's papers of the '30s] the distinction was unusual.
let me conclude by discussing one thing that seems quite revealing of this change in viewpoint: the evolution of our intuitive understanding of Gödel's completeness theorem. It is now common to present the completeness theorem [...], according to which its main intuitive content concerns the coincidence of syntactic and semantic characterizations of the consequence relation. On this reading, the natural way to state the theorem is the following:
(16) If $\Sigma \vDash \varphi$, then $\Sigma \vdash \varphi$.
What is not widely recognized is that this is a relatively late construal of Gödel's results, indeed one that seems, not surprisingly, to have originated with Tarski. Prior to this, the results were presented in one of two forms. The first derived its interest directly from the Frege-Russell conception of logic, and the question of whether the chosen logical axioms had as consequences the entire body of truths in question. Gödel's own descriptions of his first result take this form:
When one provides an axiomatic foundation for logic, as, for example, is done in Principia mathematica, the question arises whether the axioms initially adopted are "complete," that is, whether they actually suffice for the formal deduction of every correct proposition of logic.
What Gödel is describing here is sometimes called the "weak" completeness theorem, which we would now state as a reduced version of (16):
(17) if $\vDash \varphi$, then $\vdash \varphi$.
In a sense, though, (17) obscures the intuitive reading Gödel gives the result, a reading that would be more faithfully captured by the following, where '$PM$' denotes the logical axioms of the Principia :
(17') If $\varphi$ is a logical truth, then $PM \vdash \varphi$.
What this statement emphasizes is that from Gödel's point of view the result addresses precisely the same question as his later incompleteness theorem, though of course about a different "body of truths" and a different set of axioms. (17') guarantees that all first-order logical truths can indeed be derived from the Principia axioms, while the incompleteness result shows that, in contrast, there are first-order arithmetical truths that are not derivable from the Peano axioms.
However neither he [Gödel], nor anyone else at the time, stated that theorem in the form later suggested by Tarski, as a justification of the extensional adequacy of the syntactic characterization of consequence. Instead, the following formulation was used:
(18) If $\Sigma$ is (syntactically) consistent, then $\Sigma$ has a model.
Though this is equivalent to (16), the early interest in this formulation had nothing to do with its relation to the notion of semantic consequence. Rather it was seen as partial response to a criticism of Hilbert made first by Frege and later by Brouwer. The criticism had to do with whether the syntactic consistency of an uninterpreted theory was sufficient to guarantee that the theory was realizable, and hence could, as Hilbert suggested, be a substitute for truth in the mathematical domain. From that perspective, the result is more aptly described as a model existence theorem, rather than a completeness theorem, and its intuitive interest is strikingly different from that of (16).
What delayed the reformulation of (18) into (16) for so long? There reasons, both of which should by now be apparent. On the one hand, Tarski had given a semantic account of consequence that was independent of logical truth, but as we have seen his account was not equivalent to the model-theoretic definition required to get from (18) to (16). But on the other hand, all other authors who analyzed consequence semantically did so through the notion of logical truth, which from the Frege-Russell perspective took priority.
Sorry for so big a post : I hope it can raise your interest.