# When do we use entailment vs implication?

I have seen both used and I have been unable to find by searching. They seem to have a similar meaning from what I have seen, however I have only seen entailment in relation to models.

– Mwax
Jul 24, 2017 at 22:57

We have to differentiate between two levels of abstraction:

• Formal Systems
• Models

and we have to differentiate between three symbols:

• $\vDash$
• $\vdash$
• $\implies$

A model is an instance of a formal system: it satisfies the rules of inference of a given formal system, satisfies any axioms the formal system imposes, and has the same grammar as the formal system.

Given a set of formulas $\Gamma$ from a formal system $FS$ and another formula $A$ we say that $\Gamma\vdash A$ if there is a formal proof in $FS$ of $A$ from $\Gamma$. This is called syntactic consequence.

Given a set of formulas $\Gamma$ from a formal system $FS$ and another formula $A$ we say that $\Gamma\vDash A$ if there is no model of $FS$ in which all members of $\Gamma$ are true and $A$ is false. This is called semantic consequence.

The thing we call implication and usually represented by $\implies$ is a logical symbol of a formal system. The formal system is where the rules of deduction regarding $\implies$ are spelled out. For instance 'conditional proof' is usually a rule of inference for a formal system which says that if $FS\cup\{T\}\vdash T'$

$\therefore T\implies T'$ (where $T$ and $T'$ are formulas). Modus ponens is another typical rule of inference that concerns $\implies$.

We sometimes use $\vdash$ with a model $\mathcal{M}$. The string of symbols $\mathcal{M}\vdash A$ means that $\mathcal{M}$ entails $A$. That is, there is a set of formulas of the formal system which $\mathcal{M}$ asserts as true, and this set syntactically implies $A$ in the formal system which $\mathcal{M}$ instantiates.

There is another usage of $\vDash$ you should know of which involves a model. The string of symbols $\mathcal{M}\vDash A$ means that $\mathcal{M}$ is a model of the formal system in which $A$ is true.

• That was very good explanation! Jan 29, 2014 at 8:34
• "The thing we call implication and usually represented by ⟹ is a logical symbol of a formal system." Regrettably, is more accurate to say that the double arrow is used by some (in many maths cultures the majority) use $\to$ or $\supset$, i.e. as an object language conditional, and by others in semi-formalized mathematical English for implies (in the sense of entails). Jan 29, 2014 at 9:27
• You can see also in the following post the answer by Peter Smith. Jan 29, 2014 at 13:49