Double turnstile

{{Short description|Mathematical symbol}} {{Hatnote|{{noitalic|⊨}} redirects here. It is not to be confused with the Korean letter{{noitalic|ㅑ}}.}} In logic, the symbol ⊨, ⊧ or <math>\models</math> is called the '''double turnstile'''. It is often read as "entails", "models", "is a '''semantic''' '''consequence''' of" or "is stronger than".<ref>{{cite book |last=Nederpelt |first=Rob |title=Logical Reasoning: A First Course |publisher=King's College Publications|year=2004| edition=3rd revised |page=62 |chapter=Chapter 7: Strengthening and weakening|isbn=0-9543006-7-X}}</ref> It is closely related to the turnstile symbol <math>\vdash</math>, 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. <math>\Gamma \vDash \varphi</math>. 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. <math>\mathcal{A} \models \Gamma</math>. This is typically done inductively along with restricting the range of a ''variable assignment'', a function mapping each variable symbol to a value in <math>\mathcal{A}</math> it might hold.<ref>Open Logic Project, [https://builds.openlogicproject.org/content/first-order-logic/first-order-logic.pdf First-order logic] (p.7). Accessed 4 January 2022.</ref> ** In this context, the semantic consequence in the previous list can be stated as "For a given model <math>\mathcal{A}</math>, if <math>\mathcal{A} \models \Gamma</math> then <math>\mathcal{A} \vDash \varphi</math>". * To denote a tautology, <math>\vDash \varphi</math>. which is to say that the expression <math>\varphi</math> 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 <math>n</math> the statement <math>\lambda \vDash n</math> means <math>\lambda</math> is a composition of <math>n</math>.

== Typography == In TeX, the turnstile symbols ⊨ and <math>\models</math> are obtained from the commands <code>\vDash</code> and <code>\models</code> respectively.

In Unicode it is encoded at {{unichar|22A8|TRUE|html=}} , and the opposite of it is {{unichar|22AD|NOT TRUE|html=}} .

In LaTeX there is the [http://www.ctan.org/tex-archive/macros/latex/contrib/turnstile 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 [http://www.tug.org/pracjourn/2007-3/buchsbaum A Tool for Logicians] is a tutorial on using this package.

== References == <references />

Category:Mathematical symbols Category:Mathematical logic Category:Logic symbols Category:Semantics Category:Logical consequence