What is the type theory judgement symbol?
-
16-10-2019 - |
Question
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?
Solution
It's called a "turnstile". See the Wikipedia article.
OTHER TIPS
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.