Double Turnstile
   HOME

TheInfoList



OR:

In
logic Logic is the study of correct reasoning. It includes both formal and informal logic. Formal logic is the study of deductively valid inferences or logical truths. It examines how conclusions follow from premises based on the structure o ...
, the
symbol A symbol is a mark, Sign (semiotics), sign, or word that indicates, signifies, or is understood as representing an idea, physical object, object, or wikt:relationship, relationship. Symbols allow people to go beyond what is known or seen by cr ...
⊨, ⊧ or \models is called the double turnstile. It is often read as " entails", " models", "is a
semantic Semantics is the study of linguistic Meaning (philosophy), meaning. It examines what meaning is, how words get their meaning, and how the meaning of a complex expression depends on its parts. Part of this process involves the distinction betwee ...
consequence of" or "is stronger than". It is closely related to the turnstile symbol \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. \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. \mathcal \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 \mathcal it might hold.Open Logic Project
First-order logic
(p.7). Accessed 4 January 2022.
** In this context, the semantic consequence in the previous list can be stated as "For a given model \mathcal, if \mathcal \models \Gamma then \mathcal \vDash \varphi". * To denote a tautology, \vDash \varphi. which is to say that the expression \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 the statement \lambda \vDash n means \lambda is a composition of n.


Typography

In
TeX Tex, TeX, TEX, may refer to: People and fictional characters * Tex (nickname), a list of people and fictional characters with the nickname * Tex Earnhardt (1930–2020), U.S. businessman * Joe Tex (1933–1982), stage name of American soul singer ...
, the turnstile symbols ⊨ and \models are obtained from the commands \vDash and \models respectively. In Unicode it is encoded at , and the opposite of it is . In
LaTeX Latex is an emulsion (stable dispersion) of polymer microparticles in water. Latices are found in nature, but synthetic latices are common as well. In nature, latex is found as a wikt:milky, milky fluid, which is present in 10% of all floweri ...
there is th
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 articl
A Tool for Logicians
is a tutorial on using this package.


See also

*
List of logic symbols In logic, a set of symbols is commonly used to express logical representation. The following table lists many common symbols, together with their name, how they should be read out loud, and the related field of mathematics. Additionally, the sub ...
* List of mathematical symbols * Turnstile


References

Mathematical symbols Mathematical logic Logic symbols Semantics Logical consequence {{typography-stub