What is the difference between ⊢ and ⊨?

I want to know the difference between ⊢ and ⊨.

http://en.wikipedia.org/wiki/List_of_logic_symbols

⊢ means ”provable” But ⊨ is used exactly the same:

A → B ⊢ ¬B → ¬A 

A → B ⊨ ¬B → ¬A

Can you present a good example where they are different? Is it like the incompleteness theorem of recursive sets that there are sentences that are true i.e. ⊨ but do not have the property ⊢ i.e. provable?

Thanks for any insight

Solution 1:

$A \models B$ means that $B$ is true in every structure in which $A$ is true. $A\vdash B$ means $B$ can be proved using $A$ as the premises. (In both cases, $A$ is a not necessarily finite set of formulas and $B$ is a formula.)

First-order logic simultaneously enjoys the following properties: There is a system of proof for which

• If $A\vdash B$ then $A\models B$ (soundness)
• If $A\models B$ then $A\vdash B$ (completeness)
• There is a proof-checking algorithm (effectiveness).
  (And it's fortunately quite a fast-running algorithm.)

That last point is in stark contrast to this fact: There is no provability-checking algorithm. You can search for a proof of a first-order formula in such a systematic way that you'll find it if it exists, and you'll search forever if it doesn't. But if you've been searching for a million years and it hasn't turned up yet, you don't know whether the search will go on forever or end next week. These are results proved in the 1930s. The non-existence of an algorithm for deciding whether a formula is provable is called Church's theorem, after Alonzo Church.

Solution 2:

I learned that $\models$ stands for semantic entailment, while $\vdash$ stands for provability in a certain proof system.

More concretely: Given a set of formulas $\Gamma$ and a formula $\varphi$ in some logic (e.g., first-order logic), $\Gamma \models \varphi$ means that every model of $\Gamma$ is also a model of $\varphi$. On the other hand, fix a proof system (e.g., sequent calculus) for that logic. Then $\Gamma \vdash \varphi$ means that there is a proof using that proof system of $\varphi$ assuming the formulas in $\Gamma$.

The relationship between $\models$ and $\vdash$ actually describes two important properties of a proof calculus: If $\Gamma \vdash \varphi$ implies $\Gamma \models \varphi$, the proof system is sound, and if $\Gamma \models \varphi$ implies $\Gamma \vdash \varphi$, it is complete. For propositional and first-order logic, there are proof systems that are both sound and complete; this is not the case for some other logics. For example, second-order logic does not admit an effective sound and complete proof system (e.g., the set of rules for a sound and complete proof system would not be decidable).

Edit: Not every proof calculus for propositional or first-order logic is both complete and sound. For example, consider the system with the following rule: $\vdash \varphi \vee \neg \varphi$ where $\varphi$ is an arbitrary formula. This is undoubtably correct, but it's also incomplete, since one cannot derive trivially true statements like $\varphi \vdash \varphi$. On the other hand, the system $\Gamma \vdash \varphi$ for arbitrary formulae $\varphi$ and formula sets $\Gamma$ is complete, but obviously incorrect.