What is "double turnstile"

n. (context logic model theory English) The $vDash$ symbol used to denote (w logical entailment semantic consequence), or the $models$ symbol used to denote the fact that the model to the left of it satisfies the set of sentences to its right.

In logic, the symbol ⊨, $\vDash$ or  ⊨  is called the double turnstile. It is closely related to the turnstile symbol  ⊢ , which has a single bar across the middle. It is often read as " entails", " models", "is a semantic consequence of" or "is stronger than". In TeX, the turnstile symbols $\vDash$ and  ⊨  are obtained from the commands \vDash and \models respectively. In Unicode it is encoded at

In LaTeX there is the turnstile package, which issues this sign in many ways, including the double turnstile, and is capable of putting labels below or above it, in the correct places. The article A Tool for Logicians is a tutorial on using this package.