# Implies vs. Entails vs. Provable

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.

-
There are by now many similar q's on math.se: math.stackexchange.com/questions/90787/…, math.stackexchange.com/questions/68932/… and many more – alancalvitti Jan 24 '13 at 21:00
I'd like to highlight a problem when you misuse them you get problematic results, or at least I did: math.stackexchange.com/questions/854752/… – dezakin Jul 4 '14 at 17:57

## 5 Answers

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.

-
It would be wise to discern between $\Rightarrow$ (logical implication) and $\rightarrow$ (logical connective). – Asaf Karagila Jan 24 '13 at 19:44
@Asaf I'm not sure I know the difference... – Trevor Wilson Jan 24 '13 at 19:45
From the textbook presentation, I feel somewhat clear about where each operator is conventionally used. However, I feel that I must be missing a lot, because I can't think of examples where substituting one of these for another would actually make a true statement false. – user287424 Jan 24 '13 at 19:47
@alancalvitti Modus Ponens is a valid rule of inference in many logics. I think we're getting off-topic here, but see en.wikipedia.org/wiki/Modus_ponens – Trevor Wilson Jan 24 '13 at 20:59
@alancalvitti By saying "Let $M$ be a model of $A$.... Therefore $B$ holds in $M$" where the stuff in between depends on the situation. – Trevor Wilson Jan 24 '13 at 21:01

@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.

-
I should point out that in Israel you see $\implies$ used for $\models$ all the time, even in basic logic courses. The $\models$ is a relation between a structure and a sentence, rather than two formulas. – Asaf Karagila Jan 24 '13 at 20:08
(1) Doesn't $A \to B$ also mean that there is no valuation which makes the premise $A$ true and the conclusion $B$ false? (2) Why isn't Modus Ponens also a sentence rather than a relation, namely: "If $A$ and $A \to B$ is true, then $B$ is true." – alancalvitti Jan 24 '13 at 20:23
@AsafKaragila Interesting. In my neck of the words, $\vDash$ gets a double use, for the relation of semantic entailment between wffs (or, officially, a set of wffs) and a wff, as in $\Gamma\vDash\varphi$, and [not unconnectedly of course] also for the modelling relation $\mathfrak{A}\vDash\varphi$. And mathmos often use $\Rightarrow$ for the conditional! – Peter Smith Jan 24 '13 at 20:27
@alancalvitti (1) A isn't a premiss in $A \to B$. Premisses of arguments are typically asserted; $A \to B$ never asserts the antecedent $A$. (2) Modus ponens is a rule, not a proposition (as Lewis Carroll long ago reminded us!). – Peter Smith Jan 24 '13 at 20:30
@PeterSmith, do the following terms (which all appear on this page) have mathematical definitions? "Premiss" "Rule" "Sentence" "Formula" "Structure" "Provable" – alancalvitti Jan 24 '13 at 20:45

If I can add a comment, starting form Peter Smith explanation :

' → ' (or '⊃') 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→B is a single conditional proposition in the object language under consideration.

"Implies" symbols (both the syntactical one : '⊢ ' and the semantical one : '⊨ ' ) are used in meta-languge to express the conseuence relation. The connection between them is established by the rule of Modus Ponens (it allows us to conclude A⊢B from ⊢A⊃B) , and by the Deduction Theorem (it allows to conclude ⊢A⊃B from A⊢B); finally, the Completeness Th establish the connection betwenn '⊢ ' and '⊨ ' .

So there is a very tight link between the three ... but they must be treated as distinct.

It is useful (for me) to think that it is possible to avoid '⊃' in the calculus (starting form Whitehead & Russell Principia Mathematica [1910]) and using only negation (¬) and disjunction (∨).

-

$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.

-

As @Trevor Wilson said, $\vdash$ which is named “turnstile” or “right tack”, belongs to the meta‑language, however, it's not always a syntactic consequence operator, it also is a semantic consequence (what @Trevor Wilson said is $\models$), at least in type theory. The model is not only ⊨ , U+22A8, named TRUE in the Unicode database, it's also ⊧ , U+22A7, precisely named MODELS, in the Unicode database. TeX and Unicode disagree here (about ⊨ and ⊧).

As @Peter Smith said, $\rightarrow$ is a functional implication. I'm adding it's related to $\supset$ in the way the former is an interpretation of the latter (one domain to another domain).

## Examples

$$\frac{\Gamma (x) = \tau}{\Gamma \vdash x : \tau}$$

The above is from type theory, $\vdash$ stands for a semantic consequence, something which can't be inferred from the syntax. In this example, $\Gamma$ stands for a typing context, which is a semantic context, not a syntactic context; there, $\Gamma$ is like a function, something computed at the meta‑level.

$$A \supset B = A \rightarrow B$$

The above is from Curry‑Howard correspondence. To make the above clearer, it appears in a context which also asserts this:

$$A \land B = A \times B$$

… where $A \times B$ is a term of functional language and lambda‑calculus, so is $A \rightarrow B$. $A \rightarrow B$, belongs to the domain of $A \times B$; and $A \Rightarrow B$ or $A \supset B$, belongs to the domain of $A \land B$.

This is the same as the previous above (same interpretation holds):

$$A \Rightarrow B = A \rightarrow B$$

The distinction is less strong than object‑level / meta‑level distinction, this is a domain distinction. Comparing “$\vdash$ vs $\Rightarrow$” to “$\Rightarrow$ vs $\rightarrow$” is a bit like comparing explicit type conversion to implicit type conversion… a comparison to be used with a lot of care, that's just to give a picture.

## Counter examples (as the OP wish)

$$A \rightarrow B$$ Where a context is $\Gamma$, the above may make sense.

$$A \vdash B$$ Where a context is $\Gamma$, the above makes no‑sense at all (means nothing).

$$A \Rightarrow B$$ $$A \rightarrow B$$ In typed lambda‑calculus (simply typed or more expressive), both of the above may be seen as the same (the latter is originally an interpretation of the former, but since, in a valid type theory the reverse interpretation is also valid). In untyped lambda‑calculus, the former do not exists, and the latter may make sense, as much as it may makes no sense.

$$\vdash A$$ You may see the above, this makes sense (to be read as “derivable from the empty context)”.

$$\rightarrow A$$ $$\Rightarrow A$$ $$\subset A$$ You will never see the above, this makes no sense.

May be completed with other examples and counter‑examples, a future day.

-