what's the difference between Syntactic consequence ⊢ and Semantic consequence ⊨ Can you help me to differentiate the Syntactic consequence $\vdash$ and Semantic consequence $\vDash$ ?
I think  $A \vdash B$  means,  "$A$ proves $B$" and  $A \vDash B$  means , if $A$ is true, then $B$ is true.
If so, what is difference $A \to B$  and  $A\vDash B$   ?
 A: $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.]
