In his exposition of FO-theory, Mendelson uses the Gen rule : $$A(x) \vdash \forall xA(x).$$
He also states the logical consequence relation : $$A ⊨ B$$ in terms of sequences : $A$ logically implies $B$ iff, in every interpretation $I$, every sequence $s$ that satisfies $A$ also satisfies $B$.
But with this definition, we have that NOT $A(x) ⊨ \forall xA(x)$.
As a consequence of Godel’s Completeness Theorem, we have that (see pag.91 – Corollary 2.20d) : if a wff $B$ is a logical consequence of a wff $A,$ then $A \vdash B$.
But the viceversa is not stated (if I am right).
I do not understand the advantages of his definition of logical consequence.
Hunter (Metalogic ) “restored the simmetry” avoiding the Gen rule.
Other textbooks more simply defined logical consequence in term of truth in an Interpretation: in this way we have that $A(x)$ is true iff $\forall xA(x)$ is true, so that $$A(x) ⊨ \forall xA(x).$$
The problem comes down to formulas with free variables. Suppose we have a formula $\phi(x,y) \equiv x = y$, and we have a structure $M$. What would it mean for $M$ to satisfy $\phi$? Well, it doesn’t really make sense, because a variable “$x$” is not given an meaning by $M$ – $x$ doesn’t denote anything, and neither does $y$. So $x = y$ has no truth value at all.
One solution is to strengthen the notion of a “model” so that it includes both a structure $M$ and a function that assigns an element of $M$ to each variable. This is essentially the method taken by Mendelson (and also by Enderton’s classic textbook on logic). Now we have a a rigorous definition of what it means for a structure $M$ and variable assignment $s$ to satisfy $\phi(x,y)$; we might write $(M,s) \models x = y$.
The other option is to keep the notion of a model the same, but change the definition of $\models$. Now, $M \models x = y$ is defined to mean that, for every variable assignment $s$, $(M,s) \models x = y$ in the sense of the previous paragraph. But of course this is not likely to hold; in this sense we with have $M \not \models x = y$ as long as $M$ has at least two elements in its domain.
These approaches give the same truth values to all sentences – they only differ for formulas that have free variables. In many areas of mathematical logic, we are mostly interested in truth values of sentences. The main area where the second convention is useful is in universal algebra, where they often look at “equational theories”. In that context, they tend to use formulas with free variables as axioms, rather than sentences without free variables. And they are interested in models where every variable assignment satisfies the formulas, not just some random variable assignment. So they often use the second convention.
I do recommend Enderton’s book for a clear presentation of the first convention, the one where $A(x)$ does not necessarily imply $(\forall x)A(x)$.
Edit I’ve rewritten completely the answer after a re-read of Mendelson’s book, apparently it has been passed from last time I’ve read that book.
As you noticed Mendelson’s definition doesn’t allow to deduce that
$$ A(x) \models \forall x A(x)$$
since it’s not said that for any given sequence (i.e. an valuation of the variables $s$ if $s$ satisfies $A(x)$ then $s$ satisfies also $\forall x A(x)$).
Suppose we use a different semantics, for instance suppose that
$$A \models B$$
means that for every interpretation that makes true $A$ makes true also $B$. From this would follows that $A(x) \models \forall x A(x)$. Nonetheless it wouldn’t follow that $A \models B$ is equivalent to $\models A \rightarrow B$, indeed that’s the case for the formulas $A(x)$ and $\forall x A(x)$: an interpretation for which $A(x)$ is one such that every sequence $s$ makes $A(x)$ true and so it must be that such interpretation makes $\forall x A(x)$ true, hence $A(x) \models \forall x A(x)$, anyway $\not \models A(x) \rightarrow \forall x A(x)$ since there are interpretations which don’t make this true.
Having that $A \models B$ iff $\models A \rightarrow B$ is a really good property that we would like to have in our logic, since it states that $\rightarrow$ subsumes logical entailment.
I suppose that there are other good proprieties that Mandelson’s definition preserve that aren’t preserved by different semantics, at the moment I can’t think about something else.
Of course you can avoid such problems if you use different semantics, for instance using semantics that doesn’t use sequences at all.
I can tell more about such semantics if you wish.