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

Solution 1:

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.

Solution 2:

@Trevor's answer makes the crucial distinctions which need to be made: there's no disagreement at all about that. Symbolically, I'd put things just a bit differently. Consider first these three:

$$\to,\quad \vdash,\quad \vDash$$

1. '$\to$' (or '$\supset$') is a symbol belonging to various formal languages (e.g. the language of propositional logic or the language of the first-order predicate calculus) to express [usually, but not always] the truth-functional conditional. $A \to B$ is a single conditional proposition in the object language under consideration.
2. '$\vdash$' is an expression added as useful shorthand to logician's English (or Spanish or whatever) -- it belongs to the metalanguage in which we talk about consequence relations between formal sentences. Unpacked, $A, A \to B \vdash B$ says in augmented English that in some relevant deductive system, there is a proof from the premisses $A$ and $A \to B$ to the conclusion $B$. (If we are being really pernickety we would write '$A$', '$A \to B$' $\vdash$ '$B$' but it is always understood that $\vdash$ comes with invisible quotes.)
3. '$\vDash$' is another expression added to logician's English (or Spanish or whatever) -- it again belongs to the metalanguage in which we talk about consequence relations between formal sentences. And e.g. $A, A \to B \vDash B$ says that in the relevant semantics, there is no valuation which makes the premisses $A$ and $A \to B$ true and the conclusion $B$ false.

As for '$\Rightarrow$', this -- like the informal use of 'implies' -- seems to be used (especially by non-logicians), in different contexts for any of these three. It is also used, differently again, for the relation of so-called strict implication, or as punctuation in a sequent. So I'm afraid you do just have to be careful to let context disambiguate. The use of the two kinds of turnstile is absolutely standardised. The use of the double arrow isn't.

Solution 3:

$A\models B$ means $B$ is true in every structure in which $A$ is true.

$A\vdash B$ means $B$ can be proved if $A$ is assumed. But what is a proof? Usually one wants to define "proof" in such a way that (1) there's an algorithm for deciding which putative proofs are really proofs; and (2) if $A\vdash B$ then $A\models B$, i.e. only those things are provable that ought to be. In many reasonable circumstances, one also has: if $A\models B$ then $A\vdash B$, i.e. everything that ought to be provable is provable.