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

• It would be wise to discern between $\Rightarrow$ (logical implication) and $\rightarrow$ (logical connective). Jan 24, 2013 at 19:44
• The former is a statement about sentences; the latter is a part of a sentence. Logical implication vs. material implication. Jan 24, 2013 at 19:48
• @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 Jan 24, 2013 at 20:59
• @alan: I am writing from my iPhone, I am currently busy with marinating my brain in alcohol in the local watering hole. I will help you (if I can) later. Jan 24, 2013 at 21:24
• @Hibou57 I have seen the symbol $\implies$ used to mean different things. I was taking it to be the logical connective of material implication, which some people instead call $\to$, because that was how I interpreted its use in the OP's question. If I hadn't been trying to match OP's terminology, all instances of $\implies$ in my answer would be $\to$ instead. May 3, 2020 at 20:13

@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. Jan 24, 2013 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." Jan 24, 2013 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! Jan 24, 2013 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!). Jan 24, 2013 at 20:30
• @PeterSmith, but they're typically defined in terms of similar terminology rather than rigorously. So it is difficult to determine their mutual consistency. For example, what does "Sentence" mean? Jan 24, 2013 at 20:57

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

An additional comment, motivated by Peter Smith's explanation :

'$$\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 formula of object language under consideration with the conditional connective as main operator.

"Implies" symbols (both the syntactical one : '$$\vdash$$' and the semantical one: '$$\vDash$$' ) are used in the meta-language to express the consequence relation.

The connection between them is established by the rule of Modus Ponens that allows us to conclude $$A \vdash B$$ from $$\vdash A \supset B$$ , and by the Deduction Theorem that allows us to conclude $$\vdash A \supset B$$ from $$A \vdash B$$.

Finally, the Completeness Theorem establish the connection betwenn '$$\vdash$$' and '$$\vDash$$'.

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

It is useful to think that it is possible to avoid '$$\supset$$' as connective (see Whitehead & Russell's Principia Mathematica (1910)) for example using only negation ($$\lnot$$) and disjunction ($$\lor$$).

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.

• I learned quite a bit from this even though I didn't ask the question. Although I will point out that statements like A⇒B=A→B should have brackets because = takes the same precedence as a lot of other logical operators. There is no order of operations for logic that is agreed upon. Although I am nick-picking a bit because everyone can understand what you wrote anyway. Jan 22, 2017 at 6:41

A $$\vdash_{i.e.}$$ B : (read B can be proven by i.e. using A) means algorithm "ie", an inference engine, can obtain B from A

A $$\models$$ B : (read A entails B) means statement B is true in all states of the world, given A is true.

Specifically, if we let A be the axioms of some system. Then:

1. The system is complete if some possible algorithm can prove all the true statements in the system. In other words, If B is true given A (axioms) means there exists some algorithm "i.e" that can prove B using A
2. The system is sound if no statement that is false in any state of the world can be proven by any inference engine given the axioms of the system. In other words, if some algorithm "i.e." proves B using A (axioms), then B is true, given A.
• material conditional $$\left(\to\right)$$
• implication$$\left(\Rightarrow\right):$$
$$\quad\to$$ is true (perhaps in an axiom system) in the current interpretation
• logical implication / (semantic) logical entailment $$\left(\models\right):$$
$$\quad\to$$ is true regardless of interpretation
• derivability / syntactic entailment $$\left(\vdash\right):$$
$$\quad\to$$ can be proven true regardless of interpretation

For example, these two claims are simultaneously plausible: \begin{align}&\forall x\;\; x=x &\Rightarrow &&\forall x\,\forall y\;\;\; x^2 -y^2 = (x+y)(x-y),\\&\forall x\;\; x=x &\not\models &&\forall x\,\forall y\;\;\; x^2 -y^2 = (x+y)(x-y) .\end{align}

P.S. Symbolic logic is an area rife with conflicting notation, terminology and even notions; my understanding is eclectically evolving.

P.P.S. To be clear: although I distinguish analytical and synthetic implication ⇒ from logical entailment ⊨, in practice I do frequently use ⇒ (which is better recognised) even when I specifically mean the latter.

• What is meant by "interpretation" here? I understand that ⇒ is a meta-proposition about a "→"-statement, basically saying "$( \forall x, ( p(x) \rightarrow q(x) ) ) = True$. So, is ⊨ even more meta? What is the context (by Hibou57) the "in all states of the world" (by Rahul Madhavan) or "in every structure" (by Michael Hardy)? I probably misunderstand if I think this means "no matter the axioms", because they are an integral part of the language I am using in the first place? Also, specifically: Why is $∀x(x=x)⊭∀x∀y(x2−y2=(x+y)(x−y))$? May 19 at 13:07
• @Make42 $\;{^2},\,+,\,-,\,()()\,$ are not logical operators; if I define $x^2:=x$ and $x+y:=x$ and $(x)(y):=x$ and $x-y:=y,$ then that ⊨ statement has a true antecedent and false consequent. On the other hand, that ⇒ statement is mathematically true. May 19 at 15:18
• So, does this mean that 1) if a claim which uses ⊨ is true then the same claim using ⇒ instead is also true? 2) once I use symbols that are not logical symbols, then I cannot use ⊨ anymore, but - given the interpretation, I might still be able to use ⇒? May 19 at 19:24
• @Make42 1. Yes. 2. No: 1=1 ⊨ 0+0=0+0 is correct. May 19 at 19:31
• I did as you asked and wrote my own question, even though it seems to be a mess. May 20 at 20:04