In type theory judgements are often presented with the following syntax:

enter image description here

My question is what is that symbol in the middle called? All the papers I've found seem to use an image rather than a unicode character so I can't look it up. I've also not found any type-theory reference which says what that symbol is (they explain what it means however).

So what character is that symbol and what is its proper name?

  • $\begingroup$ Note that $\models$ \models is also often used in logics. $\endgroup$ – Raphael Jun 22 '12 at 9:37
  • $\begingroup$ @Raphael: $\models$ is used for semantic relationships. $\vdash$ is used for syntactic relationships, such as in proof systems. $\endgroup$ – Dave Clarke Jun 22 '12 at 9:43
  • $\begingroup$ @DaveClarke: Of course, I did not want to suggest otherwise. My intention was to leave the trail to $\models$ here, too, as you might also want to type that one if you do logics. (I know we did some weird foo before knowing \models...) $\endgroup$ – Raphael Jun 22 '12 at 9:49
  • $\begingroup$ It's a good trail to follow. $\endgroup$ – Dave Clarke Jun 22 '12 at 9:56
  • $\begingroup$ Yes, that symbol appears often as well. These comments save me another question about it. :) $\endgroup$ – edA-qa mort-ora-y Jun 23 '12 at 3:46

It's called a "turnstile". See the Wikipedia article.



Draw the character on Detexify to see what (La)TeX command generates it.

Oddly, I can't get Detexify to recognize this character. \vdash comes up eventually, but with a very bad score no matter how well I try to draw it.


Draw the character on Shapecatcher to see what it is in Unicode. It's U+22A2 RIGHT TACK (⊢).

The usual name in math is turnstile. In this context, it's sometimes called the inference symbol or the deduction symbol. The $\Gamma$ on the left is a context or environment.

  • $\begingroup$ Shapecatcher is nice. So many symbols. I also trained Detexify until it now comes up near the top. $\endgroup$ – edA-qa mort-ora-y Jun 22 '12 at 3:03
  • $\begingroup$ I couldn't help but try Detexify. I couldn't get it to recognise $\vdash$ either. Grrr. $\endgroup$ – Dave Clarke Jun 22 '12 at 9:43
  • $\begingroup$ Too many badly drawn crosses trained. $\endgroup$ – Raphael Jun 22 '12 at 9:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.