My book (Mendelson) states this theorem the following way:
(1) A logically valid formula of a first order theory is a theorem.
On Wikipedia the statement is a little more general:
(2) For any first-order theory T with a well-orderable language, and any sentence s in the language of the theory, there is a formal proof of s in T if and only if s is satisfied by every model of T.
Now “well-orderable language” is implicit in (1), and the “only if” part is fairly obvious. My doubt is about the hypothesis of “validity” used in (1) which is stronger than “true in any model” used in (2).
Because you can have an interpretation of a 1st order language which satisfies all the logic axioms, but doesn’t satisfy proper axioms, so isn’t a model of the theory. Basically valid means true under any interpretation, and there are more interpretations than models.
Am I understanding this right? Is the stronger hypothesis of (1) strictly required? Or it is also possible to prove the theorem:
(1’) A formula true in any model of a first order theory is a theorem.