Misplaced Pages

Double turnstile

Article snapshot taken from Wikipedia with creative commons attribution-sharealike license. Give it a read and then ask your questions in the chat. We can research this topic together.
Mathematical symbol ⊨ redirects here. It is not to be confused with the Korean letter.

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'.

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 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.

See also

References

  1. Nederpelt, Rob (2004). "Chapter 7: Strengthening and weakening". Logical Reasoning: A First Course (3rd revised ed.). King's College Publications. p. 62. ISBN 0-9543006-7-X.
  2. Open Logic Project, First-order logic (p.7). Accessed 4 January 2022.
Common logical symbols
 or  & and or ¬  or  ~ not implies implies,
superset
 or  iff | nand universal
quantification
existential
quantification
true,
tautology
false,
contradiction
entails,
proves
entails,
therefore
therefore because
Philosophy portal
icon Mathematics portal


Stub icon

This mathematical logic-related article is a stub. You can help Misplaced Pages by expanding it.

Stub icon

This logic-related article is a stub. You can help Misplaced Pages by expanding it.

Stub icon

This typography-related article is a stub. You can help Misplaced Pages by expanding it.

Categories: