Turnstile (symbol)
From Wikipedia, the free encyclopedia
In mathematical logic and computer science the symbol 
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 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
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]
[edit] Notes
- ^ The article on the Begriffsschrift describes its notation in detail.
- ^ See the Unicode standard at http://unicode.org/charts/PDF/U2200.pdf
- ^ A. S. Troelstra, A. S. and Schwichtenberg, H. Basic Proof Theory, second edition. Cambridge University Press, 2000. ISBN 978-0-521-77911-1
- ^ http://www.mscs.dal.ca/~selinger/papers/lambdanotes.pdf
- ^ http://dingo.sbs.arizona.edu/~hammond/ling178-sp06/mathCh6.pdf
