What is the meaning of the double turnstile symbol ($\models$)?

Solution 1:

Just to enlarge on Harry's answer:

Your symbol denotes one of two specified notions of implication in formal logic

$\vdash$ -the turnstile symbol denotes syntactic implication (syntactic here means related to syntax, the structure of a sentence), where the 'algebra' of the logical system in play (for example sentential calculus) allows us to 'rearrange and cancel' the stuff we know on the left into the thing we want to prove on the right.

An example might be the classic "all men are mortal $\wedge$ socrates is a man $\vdash$ socrates is mortal" ('$\wedge$' of course here just means 'and'). You can almost imagine cancelling out the 'man bit' on the left to just give the sentence on the right (although the truth may be more complex...).

$\models$ -the double turnstile, on the other hand, is not so much about algebra as meaning (formally it denotes semantic implication)- it means that any interpretation of the stuff we know on the left must have the corresponding interpretation of the thing we want to prove on the right true.

An example would be if we had an infinite set of sentences: $\Gamma$:= {"1 is lovely", "2 is lovely", ...} in which all numbers appear, and the sentence A= " the natural numbers are precisely {1,2,...}" listing all numbers. Any interpretation would give us B="all natural numbers are lovely". So $\Gamma$, A $\models$ B.

Now, the goal of any logician trying to set up a formal system is to have $\Gamma \vdash A \iff \Gamma \models A$, meaning that the 'algebra' must line up with the interpretation, and this is not something we can take as given. Take the second example above- can we be sure that algebraic operations can 'parse' those infinitely many sentences and make the simple sentence on the right?? (this is to do with a property called compactness)

The goal can be split into two distict subgoals:

Soundness: $A \vdash B \Rightarrow A \models B$

Completeness: $A \models B \Rightarrow A \vdash B$

Where the first stops you proving things that aren't true when we interpret them and the second means that everything we know to be true on interpretation, we must be able to prove.

Sentential calculus, for example, can be proved complete (and was in Godel's lesser known, but celebrated completeness theorem), but other for other systems Godel's incompleteness theorem, give us a terrible choice between the two.

In summary: The interplay of meaning and axiomatic machine mathematics, captured by the difference between $\models$ and $\vdash$, is a subtle and interesting thing.

Solution 2:

$\models$ is also known as the satisfication relation. For a structure $\mathcal{M}=(M,I)$ and an $\mathcal{M}$-assignment $\nu$, $(\mathcal{M},\nu)\models \varphi$ means that the formula $\varphi$ is true with the particular assignment $\nu$.
See http://www.trinity.edu/cbrown/topics_in_logic/struct/node2.html