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.