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.
Solution 1:
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.