Turnstile (symbol)
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. It is also referred to as tee and is often read as "yields", "proves", "satisfies" or "entails". The symbol was first used by Gottlob Frege
in his 1879 book on logic, Begriffsschrift
.
In TeX
, the turnstile symbol
is obtained from the command \vdash. In Unicode
, the turnstile symbol is called right tack and is at code point U+22A2. On a typewriter
, a turnstile can be composed from a vertical bar
(|) and a dash
(-). In LaTeX
there is the turnstile package, which issues this sign in many ways, 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.
Mathematical logic
Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...
and computer science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
the symbol
has taken the name turnstile because of its resemblance to a typical turnstileTurnstile
A turnstile, also called a baffle gate, is a form of gate which allows one person to pass at a time. It can also be made so as to enforce one-way traffic of people, and in addition, it can restrict passage only to people who insert a coin, a ticket, a pass, or similar...
if viewed from above. It is also referred to as tee and is often read as "yields", "proves", "satisfies" or "entails". The symbol was first used by Gottlob Frege
Gottlob Frege
Friedrich Ludwig Gottlob Frege was a German mathematician, logician and philosopher. He is considered to be one of the founders of modern logic, and made major contributions to the foundations of mathematics. He is generally considered to be the father of analytic philosophy, for his writings on...
in his 1879 book on logic, Begriffsschrift
Begriffsschrift
Begriffsschrift is a book on logic by Gottlob Frege, published in 1879, and the formal system set out in that book...
.
In TeX
TeX
TeX is a typesetting system designed and mostly written by Donald Knuth and released in 1978. Within the typesetting system, its name is formatted as ....
, the turnstile symbol
is obtained from the command \vdash. In UnicodeUnicode
Unicode is a computing industry standard for the consistent encoding, representation and handling of text expressed in most of the world's writing systems...
, the turnstile symbol is called right tack and is at code point U+22A2. On a typewriter
Typewriter
A typewriter is a mechanical or electromechanical device with keys that, when pressed, cause characters to be printed on a medium, usually paper. Typically one character is printed per keypress, and the machine prints the characters by making ink impressions of type elements similar to the pieces...
, a turnstile can be composed from a vertical bar
Vertical bar
The vertical bar is a character with various uses in mathematics, where it can be used to represent absolute value, among others; in computing and programming and in general typography, as a divider not unlike the interpunct...
(|) and a dash
Dash
A dash is one of several kinds of punctuation mark. Dashes appear similar to hyphens, but differ from them primarily in length, and serve different functions. The most common versions of the dash are the en dash and the em dash .-Common dashes:...
(-). In LaTeX
LaTeX
LaTeX is a document markup language and document preparation system for the TeX typesetting program. Within the typesetting system, its name is styled as . The term LaTeX refers only to the language in which documents are written, not to the editor used to write those documents. In order to...
there is the turnstile package, which issues this sign in many ways, 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.
Meaning
The turnstile is a binary relation. It has several different meanings in different contexts:- In proof theoryProof theoryProof theory is a branch of mathematical logic that represents proofs as formal mathematical objects, facilitating their analysis by mathematical techniques. Proofs are typically presented as inductively-defined data structures such as plain lists, boxed lists, or trees, which are constructed...
, the turnstile is used to denote provability. For example, if T is a formal theoryFormal theoryFormal theory can refer to:* Another name for a theory which is expressed in formal language.* An axiomatic system, something representable by symbols and its operators...
and S is a particular sentence in the language of the theory then
means that S is provable from T. This usage is demonstrated in the article on propositional calculusPropositional calculusIn mathematical logic, a propositional calculus or logic is a formal system in which formulas of a formal language may be interpreted as representing propositions. A system of inference rules and axioms allows certain formulas to be derived, called theorems; which may be interpreted as true...
. - In the typed lambda calculusTyped lambda calculusA typed lambda calculus is a typed formalism that uses the lambda-symbol to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a type depends on the calculus considered...
, the turnstile is used to separate typing assumptions from the typing judgement. - In the study of formal languageFormal languageA formal language is a set of words—that is, finite strings of letters, symbols, or tokens that are defined in the language. The set from which these letters are taken is the alphabet over which the language is defined. A formal language is often defined by means of a formal grammar...
s, the turnstile represents syntactic consequence. This is to say that it shows that one string can be derivedFormal proofA formal proof or derivation is a finite sequence of sentences each of which is an axiom or follows from the preceding sentences in the sequence by a rule of inference. The last sentence in the sequence is a theorem of a formal system...
from another in a single step, according to the rulesRule of inferenceIn logic, a rule of inference, inference rule, or transformation rule is the act of drawing a conclusion based on the form of premises interpreted as a function which takes premises, analyses their syntax, and returns a conclusion...
for the formal language. - In category theoryCategory theoryCategory theory is an area of study in mathematics that examines in an abstract way the properties of particular mathematical concepts, by formalising them as collections of objects and arrows , where these collections satisfy certain basic conditions...
, a reversed turnstile (⊣), as in
, is used to indicate that the functorFunctorIn category theory, a branch of mathematics, a functor is a special type of mapping between categories. Functors can be thought of as homomorphisms between categories, or morphisms when in the category of small categories....
is left adjoint to the functor 
.