# Implies ($\Rightarrow$) vs. Entails ($\models$) vs. Provable ($\vdash$)

Consider A $\Rightarrow$ B, A $\models$ B, and A $\vdash$ B.

What are some examples contrasting their proper use? For example, give A and B such that A $\models$ B is true but A $\Rightarrow$ B is false. I’d appreciate pointers to any tutorial-level discussion that contrasts these operators.

Edit: What I took away from this discussion and the others linked is that logicians make a distinction between $\vdash$ and $\models$, but non-logicians tend to use $\Rightarrow$ for both relations plus a few others. Points go to Trevor for being the first to explain the relevance of completeness and soundness.

First let’s compare $A \implies B$ with $A \vdash B$. The former is a statement in the object language and the latter is a statement in the meta-language, so it would make more sense to compare $\vdash A \implies B$ with $A \vdash B$.
The rule of modus ponens allows us to conclude $A \vdash B$ from $\vdash A \implies B$, and the deduction theorem allows to conclude $\vdash A \implies B$ from $A \vdash B$. Probably there are exotic logics where modus ponens fails or the deduction theorem fails, but I’m not sure that’s what you’re looking for.
I think the short answer is that if you put a turnstile ($\vdash$) in front of $A \implies B$ to make it a statement in the meta-language (asserting that the implication is provable) then you get something equivalent to $A \vdash B$.
Next let’s compare $A \vdash B$ with $A \models B$. These are both statements in the meta-language. The former asserts the existence of a proof of $B$ from $A$ (syntactic consequence) whereas the latter asserts that every $B$ holds in every model of $A$ (semantic consequence). Whether these are equivalent depends on what class of models we allow in our logical system, and what deduction rules we allow. If the logical system is sound then we can conclude $A \models B$ from $A \vdash B$, and if the logical system is complete then we can conclude $A \vdash B$ from $A \models B$. These are desirable properties for logical systems to have, but there are logical systems that are not sound or complete. For example, if you remove some essential rule of inference from a system it will cease to be complete, and if you add some invalid rule of inference to the system it will cease to be sound.