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


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

4 Answers 4


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

  • $\begingroup$ 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!? $\endgroup$ Jul 22, 2010 at 12:12
  • $\begingroup$ TeX fixed - see meta.math.stackexchange.com/questions/692/… $\endgroup$
    – Larry Wang
    Sep 16, 2010 at 21:52
  • $\begingroup$ @TomBoardman Thank you for your answer but think it can be more complete if you also explained about the meaning of double turnstile in different contexts, as explained in "en.wikipedia.org/wiki/Double_turnstile". (Showing tautology, sastisfaction and semantic consequence) $\endgroup$
    – Saber
    Feb 28, 2018 at 16:42
  • 2
    $\begingroup$ About the $\vDash$ example. How can "any interpretation" be correct? If I interpret some words differently, it can become nonsense (for example an interpretation where "precisely" means "not"). But I'm not sure if I understand the underlying concepts. $\endgroup$
    – dekuShrub
    May 14, 2020 at 9:28
  • $\begingroup$ this is a rather vague explanation $\endgroup$ Nov 6, 2023 at 5:22

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

  • $\begingroup$ Are you ever coming back? Just curious... :) $\endgroup$ Mar 27, 2012 at 4:49
  • $\begingroup$ Are you coming back anytime soon? $\endgroup$
    – Hyperbola
    Oct 30, 2016 at 1:26

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.

  • $\begingroup$ 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. $\endgroup$
    – bryn
    Jul 22, 2010 at 11:22
  • $\begingroup$ @bryn: Not that I've seen. Forcing uses two vertical lines. $\endgroup$ Jul 22, 2010 at 12:34
  • $\begingroup$ As a related question, what does the 'single turnstile' mean? I've seen it plenty of times. $\endgroup$
    – Noldorin
    Jul 22, 2010 at 16:19
  • $\begingroup$ Is it equivalent toe the single or double tailed right-arrows in logic? $\endgroup$
    – Noldorin
    Jul 22, 2010 at 16:28
  • $\begingroup$ @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. $\endgroup$
    – bryn
    Jul 22, 2010 at 22:12

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .