Turnstile (symbol)

From Wikipedia, the free encyclopedia

In mathematical logic and computer science the symbol $\vdash$ has taken the name turnstile because of its resemblance to a typical turnstile if viewed from above. The symbol was first used by Gottlob Frege in his Begriffsschrift.^[1]

In TeX, the turnstile symbol $\vdash$ is obtained from the command \vdash. In Unicode, the turnstile symbol ├ is called right tack and is at point 0x22A2. ^[2] On a typewriter, a turnstile can be composed from a vertical bar (|) and a dash (-).

[edit] Meaning

The turnstile is a binary relation. It has several different meanings in different contexts:

In proof theory, the turnstile is used to denote provability. For example, if T is a formal theory and S is a particular sentence in the language of the theory then $T \vdash S$ means that S is provable from T.^[3] This usage is demonstrated in the article on propositional calculus.
In the typed lambda calculus, the turnstile is used to represent the steps in type resolution algorithms. ^[4]
In the study of formal languages, the turnstile is used to show that one string can be derived from another in a single step, according to the rules for the formal language. ^[5]