what's the difference between Syntactic consequence ⊢ and Semantic consequence ⊨ [duplicate]

Solution 1:

$A \vdash_S B$ means there is a derivation, in the proof-system $S$, from the premise $A$ to the conclusion $B$. [If context fixes the relevant system $S$ we suppress the subscript.]

$A \vDash_L B$ means that on every possible interpretation of the non-logical vocabulary of language $L$, if $A$ comes out true, so does $B$. [If context fixes the relevant language $L$ we suppress the subscript.]

Both those are metalinguistic claims, the symbolism abbreviating mathematical English (or mathematical Spanish, or whatever), making claims about the relation between the well-formed formulas (wffs) $A$ and $B$, looking from the outside of their formal language, so to speak.

$A \to B$, by contrast, is a wff that belongs to the object language, to the formal language of which $A$ and $B$ are wffs (typically, but far from always, interpreted as expressing the truth-functional conditional).

On the truth-functional interpretation, if the atomic wff $p$ happens to be false and the atomic wff $q$ happens to be false too, then $p \to q$ evaluates as true. But of course we don't have $p \vDash q$ ($q$ isn't true on every valuation which makes $p$ true).

And so it goes ......

[Oh, I seem to have said much the same before, in slightly different words, at https://math.stackexchange.com/questions/286077/implies-vs-entails-vs-provable, so check that out too to see whether that helps as well.]