In logic, the symbol ⊨, ⊧ or ⊨ {\displaystyle \models } 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 ⊢ {\displaystyle \vdash }, 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:

  • To show semantic consequence, with a set of sentences on the left and a single sentence on the right, to denote that if every sentence on the left is true, the sentence on the right must be true, e.g. Γ ⊨ φ {\displaystyle \Gamma \vDash \varphi }. This usage is closely related to the single-barred turnstile symbol which denotes syntactic consequence.
  • To show satisfaction, with a model (or truth-structure) on the left and a set of sentences on the right, to denote that the structure is a model for (or satisfies) the set of sentences, e.g. A ⊨ Γ {\displaystyle {\mathcal {A}}\models \Gamma }. This is typically done inductively along with restricting the range of a variable assignment, a function mapping each variable symbol to a value in A {\displaystyle {\mathcal {A}}} it might hold. In this context, the semantic consequence in the previous list can be stated as "For a given model A {\displaystyle {\mathcal {A}}}, if A ⊨ Γ {\displaystyle {\mathcal {A}}\models \Gamma } then A ⊨ φ {\displaystyle {\mathcal {A}}\vDash \varphi }".
  • To denote a tautology, ⊨ φ {\displaystyle \vDash \varphi }. which is to say that the expression φ {\displaystyle \varphi } is a semantic consequence of the empty set.
  • You can also use this symbol as follows: ⊭ to denote the statement 'does not entail'.
  • There is an unrelated usage in combinatorics where for a non-negative integer n {\displaystyle n} the statement λ ⊨ n {\displaystyle \lambda \vDash n} means λ {\displaystyle \lambda } is a composition of n {\displaystyle n}.

Typography

In TeX, the turnstile symbols ⊨ and ⊨ {\displaystyle \models } are obtained from the commands \vDash and \models respectively.

In Unicode it is encoded at U+22A8⊨ TRUE (⊨, ⊨) , and the opposite of it is U+22AD⊭ NOT TRUE (⊭) .

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.

See also