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

What's the meaning of the double turnstile symbol in logic or mathematical notation? :

$\models$

-
@Harry: Not too localised, if any model-theory questions are not too localised. – Charles Stewart Jul 22 '10 at 11:36
As a general comment, I recommend using detexify (detexify.kirelabs.org/classify.html) and Wikipedia to help first. – Akhil Mathew Jul 22 '10 at 11:45
The value is limited as we can't exactly search for this question – Casebash Jul 22 '10 at 12:24
@Casebash: Why not edit the title to "what is the meaning of the 'double turnstile' symbol in logic?" ? – Tom Boardman Jul 26 '10 at 13:42
I voted to re-open, since I don't understand why it was closed in the first place. – JDH Feb 26 '12 at 14:27

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.

-
Gosh, wrote a lot more than I intended there, but it is jolly interesting... now can someone please tell me how to fix my Tex!? – Tom Boardman Jul 22 '10 at 12:12
TeX fixed - see meta.math.stackexchange.com/questions/692/… – Larry Wang Sep 16 '10 at 21:52

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

-
Are you ever coming back? Just curious... :) – The Chaz 2.0 Mar 27 '12 at 4:49

It is a symbol from model theory denoting entailment.

A ⊧ B is read as "A entails B".

-

It is called a 'double turnstile': http://en.wikipedia.org/wiki/Double_turnstile.

-
Sorry, I realise that I haven't actually answered your question (about the meaning). I've seen it used in logic to stand for semantic entailment, but I imagine it has other uses. – bryn Jul 22 '10 at 11:22
@bryn: Not that I've seen. Forcing uses two vertical lines. – Charles Stewart Jul 22 '10 at 12:34
As a related question, what does the 'single turnstile' mean? I've seen it plenty of times. – Noldorin Jul 22 '10 at 16:19
Is it equivalent toe the single or double tailed right-arrows in logic? – Noldorin Jul 22 '10 at 16:28
@Noldorin, perhaps the simplest example of the distinction could be seen in classical propositional logic. A statement like |= p -> (q -> p) means that the no matter the truth values of p and q, the value of p -> (q -> p) is always truth (which can be seen by looking at the truth table). A statement like |- p -> (q -> p) means that we can prove this formula purely by using axioms/rules of deduction, with no mention of truth or meaning. Incidentally, I think you could ask this as a separate question on the site, since we don't want the comment strand to be where one has to look for answers. – bryn Jul 22 '10 at 22:12