[Math] the difference between ⊢ and ⊨

logicproof-theory

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

Best Answer

$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.

Related Question