Double turnstile

Not to be confused with ㅑ.

In logic, the symbol $\vDash$ 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 "models" or "is a semantic consequence of". In TeX, the turnstile symbol $\vDash$ is obtained from the command \vDash. The unicode html entity is ⊨.

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.

Meaning

The turnstile is a binary relation. It has several different meanings in different contexts:

• In logic, the double turnstile is used to denote semantic consequence. In this context, it is closely related to the turnstile symbol which denotes syntactic consequence.