This, “⊢”, is the turnstile. At least some logicians use ‘turnstile’ informally for the name of this symbol in those rare places where they explain the meaning that they ascribe to it. How do you look up the meaning of such a glyph? On the web such characters are often displayed in Unicode and then a page such as this may help. Copy and paste the mysterious symbol into the text box on that page and type return. You should see this page for the turnstile. This tells you that the numeric code-point for the turnstile is hexadecimal 22A2 in Unicode.

That code-point information can be used at this site to find the name of the neighborhood and the name that the Unicode committee gave the glyph as they assigned its code-point. They called our symbol “RIGHT TACK” but also gave alternate names including “turnstile” which might be known to a web search engine. Indeed “RIGHT TACK” is not productive with search engines but with a bit of luck “turnstile” will get you to this Wikipedia page. I expand here on the logical usage alluded to in that article.

The logician who is concerned with what follows from what, and especially what follows from some particular set of axioms will write “Γ ⊢ A” where Γ describes the axioms, given elsewhere by naming some set of assertions or propositions, and A is some particular proposition. The meaning of the compound expression is that according to some set of deduction rules under discussion, A may be deduced from statements in Γ. Often the Γ is omitted when the discussion is in context of a particular set of axioms and then “⊢ A” means that A may be deduced from those axioms, i.e. that A is a theorem in the formal system. Sometimes more than one set of deduction rules are under discussion and then there will be a subscript to the turnstile. The simplest and most common deduction rule is merely modus ponens.