I see that the double turnstile ⊨ denotes the semantic consequence of some sentence of logic, and single turnstile ⊢ denotes the syntactic consequence of some model. This seems equivalent to me. Why do we need to make this distinction? Are there cases where P⊢Q but P!⊨(does not entail) Q?
Interesting question! You used the word 'model' when describing the turnstile, so I'll start with these:
Models are a semantical notion, so the use of 'model' needs to be avoided in the characterization of syntactic consequence. Now that we're clearer about the definitions of the two types of consequence, I hope you can see that it's not at all obvious that the notions of provability and truth coincide. Significant effort goes into proving the equivalence between a proof system and a semantics for many logics.
Take propositional logic, for example. It has a proof system, the so-called propositional calculus, and a semantics, the so-called truth-tables. The propositional calculus captures the notion of syntactic consequence, truth-tables the notion of semantic consequence. A routine exercise in introductory logic courses is to show that the propositional calculus, in some presentation, is sound with respect to the truth-tables, i.e. that:
Although the proof is easy, it still needs to be shown; otherwise we'd have to take it on faith that our axioms (if we have any) are true and that our rules of inference are truth-preserving. Similarly for the converse direction, which is called completeness:
This one is usually much harder to prove, and is important because we want the proof system to capture or prove all the truths our semantics generates. Propositional logic enjoys both properties, but there are logics for which such proofs either have not yet been or cannot be devised.
We need the distinction because the two concepts are different [see Hunan's explanation].
There are theorems regarding the equivalence between the two concepts both for propositional logic (see : Soundness and completeness of the rules) and first-order logic (see : Gödel's completeness theorem ).
For second-order logic this is not true anymore.
See also this post.