Double turnstile

In logic, the symbol ⊨, ⊧ or formula_1 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 formula_2, which has a single bar across the middle, and which denotes "syntactic" consequence (in contrast to "semantic").
Meaning.
The double turnstile is a binary relation. It has several different meanings in different contexts:
Typography.
In TeX, the turnstile symbols formula_10 and formula_1 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.