According to Wikipedia:
A logical consequence is the relationship between statements that holds true when one logically "follows from" one or more others.
So,
A ⊨ B
B is a logical consequence of A when in all cases of A being true, B is true as well.
However, to my understanding, that is also what implication means.
A → B
B should be true whenever A is true. Isn't that the same as entailment?
$\endgroup$ 21 Answer
$\begingroup$As said in the above comment, $A \to B$ is a formula in the language (e.g. propositional calculus) while $\varphi \vDash \psi$ is a relation between formulae, and thus it is an expression in the meta-language.
It is true that $A \vDash B$ iff $\vDash A \to B$, but still the difference is important.
We may have, e.g., a language with only $\lnot$ and $\lor$ conncetives; in it the definition of well-formed formula changes ($A \to B$ must be introduced as an abbreviation) while the definition of $\vDash$ does not.
In addition, the relation $\vDash$ holds also with a set $\Gamma$, possibly infinite, of formulae :
$\Gamma \vDash \varphi$,
while $\gamma \to \varphi$, being a formula, must be a finite string, and thus the antecedent $\gamma$ can be at most a finite conjunction.
$\endgroup$ 2
