patternMinor
What is the type theory judgement symbol?
Viewed 0 times
judgementthewhattheorysymboltype
Problem
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?
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
Detexify
Draw the character on Detexify to see what (La)TeX command generates it.
Oddly, I can't get Detexify to recognize this character.
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.
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.
Context
StackExchange Computer Science Q#2437, answer score: 4
Revisions (0)
No revisions yet.