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

-

4 Answers

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

-
Finally I understand what Church's theorem means. I'm going to look more closely at how it is proven that there is no proff-finding algorithm. Thank you for the answer. –  Niklas rtz May 22 '12 at 14:36
I've rephrased the last sentence of the answer a bit, no longer referring to it as a "proof-finding algorithm". In one sense, there is a "proof-finding algorithm": it will find a proof if one exists. But there is no algorithm for deciding whether a proof exists. –  Michael Hardy May 22 '12 at 14:42
@NickRosencrantz : Now I'm wondering if I was right as to which theorem is most conventionally called Church's theorem. I think it may be the one that says there's no algorithm for deciding which first-order formulas are universally valid. –  Michael Hardy Mar 20 '13 at 11:46
Very interesting. I wanted to know this for 15 years. –  Niklas rtz Mar 20 '13 at 11:50

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.

-

Michael Hardy and Johannes Kloos have answered this already, but I thought a typical example might illuminate the point further. $\def\ra{\rightarrow}$

Let's consider propositional logic and say that $S$ is some formula of propositional logic, perhaps $p\ra(p\ra q)\ra q$ or $p\ra q$. We can make a truth table of the values of $S$ for each possible valuation of its variables. If the truth table says that $S$ is true regardless of the values we assign to the variables, then we will say that $S$ is a tautology, and write $\vDash S$.

Now let's consider the following system of axioms: $$X\ra (Y\ra X) \\ (X\ra(Y\ra Z))\ra((X\ra Y)\ra(X\ra Z))$$

where $X$, $Y$, and $Z$ may be any well-formed formulas, and the modus ponens deduction rule, which says that if we can prove $X$ and we can prove $X\ra Y$, then we can prove $Y$.

If we can prove some sentence $S$ from these axioms and this deduction rule, we will say that $S$ is a theorem, and write $\vdash S$.

This would be a typical use of $\vdash$ and $\vDash$.

It should be clear that it is not at all obvious that $\vdash$ and $\vDash$ mean the same thing; they are defined quite differently. Perhaps you can imagine trying to prove that they mean the same thing.

In fact as I defined them, they do not mean the same thing! It is the case that $\vDash p\vee\lnot p$, but I gave no axioms that would allow one to deduce $\vdash p\vee\lnot p$. Every deducible theorem has a $\ra$ in it somewhere!

Or to take a less silly example, it turns out that $\vDash ((p\ra q)\ra p)\ra p$ but not $\vdash ((p\ra q)\ra p)\ra p$.

As it happens, we have $\vdash T$ implies $\vDash T$, but not necessarily the converse. If we add $(p\ra q)\ra p)\ra p$ to the set of axiom schemas, and agree that $\vDash T$ applies only to formulas whose only operator is $\ra$, then the axiom system becomes stronger and there are fewer tautologies, and $\vdash T$ and $\vDash T$ become equivalent.

-

Here is a wikipedia article with a comprehensive list of logic symbols and their meanings.

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

-