I was asked about the differences between the two symbols by a student.

p => q * (1)
*

and

p |= q *(2)*

The first one is a material implication, or whatever people call it, which expresses a binary truth function in propositional logic. So, in propositional logic, we can build a truth table to see if (1) holds. This definition is not often desired because as we know q can be anything when p is false, and this is still a tautology. Some claim that this is paradoxical (cf. Wikipedia).

A simple way to understand: (1) p=>q is merely a shorthand (logical equivalence) for ~p \/ q, which means that they can be used interchangebly.A material implication is truth-preserving, and that is what it does.

In predicate logic, I understand (1) as follows. The two sets are compared in terms of the extensions of the two sets, e.g.,

A = {forall x: x>0}

B = {forall x: x>-1}

then we say A=>B.

People claim that (1) introduces paradox (see wikipedia) because this sort of implication does not exclude apparent contradictions, e.g.,

"4 is odd => 4 is even" *(3)*

is true. So, it is said that (1) does not correspond to "if p then q", but rather "not p or q".

However, a paper by Ceniza in 1988 suggested that *(3)* is not a paradox because from the material implication (1) we can in fact get the following formula:

q \/ p => q *(4)*

So (3) is a tautology because the material implication has put the consequent (that is, q) implicitly in the antecedent, which has nothing to do with the false antecedent (p here) as q implies/entails itself here! I make no comment on this paper, and include this for the sake of completeness only.

(2) is also called entailment , logical implication, semantic implication, logical consequence, etc. because it relates to the model theory saying that every model/interpretation of p is also a model of q. This is somewhat stronger than (1) from the semantic point of view. An explanation follows.

Entailment like "p1, p2, ... pk |= q" states that whenever the vaulation makes p1, p2, ..., pk true, then it must make q true. That is, the conclusion follows deductively from the
premises. This does not mean that the conclusion is true, as the premises can be false [cf. Tarski]. Entailment means it is **impossible **for this case to occur: the premises are true **and **the consequence is false.

In deductive systems, the *deduction theorem* applies to most logics (but not all): if p|= q then EMPTY |= (p => q), and vice versa. So another understanding in these systems caan be: an entailment like p|= q states that (p => q) is always true, or a tautalogy.

Note that implication is in the logic itself (it is normally defined as an operator/connective of the logic), while entailment is in the **meta-logic** (a language used to desscribe some properties of a logic!).

**Added notes for beginners**:

The symbol called proof or consequence |- is obvious different from |=, the logical consequence. A proof manipulates the structure (syntax) of formulas, and tries to reach another formula by referring to a set of rules. If indeed such a proof is found, we say from the premises we can conclude the consequent.

Logical consequence, or entailment instead looks at the model/valuation of formulas in the premises and that of the conclusion.

In a nutshell, consequence (denoted by |- ) is syntactic, while entailment (denoted by |= ) is related to semantics, thus semantic.