5
$\begingroup$

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?

Improve this question
$\endgroup$
5
  • $\begingroup$ Note that $\models$ \models is also often used in logics. $\endgroup$
    – Raphael
    Commented Jun 22, 2012 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
    Commented Jun 22, 2012 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
    Commented Jun 22, 2012 at 9:49
  • $\begingroup$ It's a good trail to follow. $\endgroup$
    – Dave Clarke
    Commented Jun 22, 2012 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
    Commented Jun 23, 2012 at 3:46

2 Answers 2

Reset to default
4
$\begingroup$

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

Improve this answer
$\endgroup$
0
4
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • $\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
    Commented Jun 22, 2012 at 3:03
  • $\begingroup$ I couldn't help but try Detexify. I couldn't get it to recognise $\vdash$ either. Grrr. $\endgroup$
    – Dave Clarke
    Commented Jun 22, 2012 at 9:43
  • $\begingroup$ Too many badly drawn crosses trained. $\endgroup$
    – Raphael
    Commented Jun 22, 2012 at 9:51

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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