Turnstile (symbol)

Turnstile (symbol)

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. It is also referred to as tee and is often read as "yields" or "proves". The symbol was first used by Gottlob Frege in his 1879 book on logic, "Begriffsschrift" [Gottlob Frege, Begriffsschrift: Eine der arithmetischen nachgebildete Formelsprache des reinen Denkens. Halle, 1879. ] .

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 [ [http://unicode.org/charts/PDF/U2200.pdf Unicode standard] ] . On a typewriter, a turnstile can be composed from a vertical bar (|) and a dash (-). In LaTeX there is the [http://www.ctan.org/tex-archive/macros/latex/contrib/turnstile 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 [http://www.tug.org/pracjourn/2007-3/buchsbaum 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 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" [A. S. Troelstra and H. Schwichtenberg, "Basic Proof Theory", second edition, Cambridge University Press, 2000, ISBN 978-0-521-77911-1.] . This usage is demonstrated in the article on propositional calculus.
* In the typed lambda calculus, the turnstile is used to separate typing assumptions from the typing judgement. [http://www.mscs.dal.ca/~selinger/papers/lambdanotes.pdf]
* 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. [http://dingo.sbs.arizona.edu/~hammond/ling178-sp06/mathCh6.pdf]

Notes


Wikimedia Foundation. 2010.

Игры ⚽ Нужна курсовая?

Look at other dictionaries:

  • Turnstile (disambiguation) — A turnstile is a pedestrian gate.Turnstile may also refer to: *Turnstile (symbol), symbol used in mathematics, logic and computer science *Turnstiles, Billy Joel album *Turnstile antenna, set of two dipole antennas *Optical turnstile, physical… …   Wikipedia

  • Double turnstile — Not to be confused with ㅑ. In logic, the symbol is called the double turnstile. It is closely related to the turnstile symbol, which has a single bar across the middle. It is often read as models or is a semantic consequence of . In TeX, the… …   Wikipedia

  • Sequent calculus — In proof theory and mathematical logic, sequent calculus is a family of formal systems sharing a certain style of inference and certain formal properties. The first sequent calculi, systems LK and LJ, were introduced by Gerhard Gentzen in 1934 as …   Wikipedia

  • Generalization (logic) — Generalization is an inference rule of predicate calculus which states that:: If vdash P(x) is true (valid) then so is vdash forall x , P(x) . Generalization can be abbreviated as GEN. The inference rule can be summarized as the sequent: P(x)… …   Wikipedia

  • Entailment — For other uses, see Entail (disambiguation). In logic, entailment is a relation between a set of sentences (e.g.,[1] meaningfully declarative sentences or truthbearers) and a sentence. Let Γ be a set of one or more sentences; let S1 be the… …   Wikipedia

  • First-order logic — is a formal logical system used in mathematics, philosophy, linguistics, and computer science. It goes by many names, including: first order predicate calculus, the lower predicate calculus, quantification theory, and predicate logic (a less… …   Wikipedia

  • Contradiction — In classical logic, a contradiction consists of a logical incompatibility between two or more propositions. It occurs when the propositions, taken together, yield two conclusions which form the logical, usually opposite inversions of each other.… …   Wikipedia

  • Rule of inference — In logic, a rule of inference (also called a transformation rule) is a function from sets of formulae to formulae. The argument is called the premise set (or simply premises ) and the value the conclusion . They can also be viewed as relations… …   Wikipedia

  • Structural proof theory — In mathematical logic, structural proof theory is the subdiscipline of proof theory that studies proof calculi that support a notion of analytic proof. Contents 1 Analytic proof 2 Structures and connectives 3 Cut elimination in the sequent… …   Wikipedia

  • List of mathematics articles (T) — NOTOC T T duality T group T group (mathematics) T integration T norm T norm fuzzy logics T schema T square (fractal) T symmetry T table T theory T.C. Mits T1 space Table of bases Table of Clebsch Gordan coefficients Table of divisors Table of Lie …   Wikipedia

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”