Double turnstile


In logic, the symbol ⊨, ⊧ or is called the double turnstile. It is often read as "entails", "models", "is a semantic consequence of" or "is stronger than". It is closely related to the turnstile symbol, which has a single bar across the middle, and which denotes syntactic consequence.

Meaning

The double turnstile is a binary relation. It has several different meanings in different contexts:
In TeX, the turnstile symbols and are obtained from the commands \vDash and \models respectively. In Unicode it is encoded at
In LaTeX there is the , 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 is a tutorial on using this package.