# What is the type theory judgement symbol?

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

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?

• Note that $\models$ \models is also often used in logics. – Raphael Jun 22 '12 at 9:37
• @Raphael: $\models$ is used for semantic relationships. $\vdash$ is used for syntactic relationships, such as in proof systems. – Dave Clarke Jun 22 '12 at 9:43
• @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...) – Raphael Jun 22 '12 at 9:49
• It's a good trail to follow. – Dave Clarke Jun 22 '12 at 9:56
• Yes, that symbol appears often as well. These comments save me another question about it. :) – edA-qa mort-ora-y Jun 23 '12 at 3:46

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

### Detexify

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.

### Shapecatcher

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.

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