Turnstile (⊢)

How to read it

The Stanford Encyclopedia of Philosophy writes Γ ⊢ φ to say that φ is deducible from Γ, and ⊢ φ, with nothing on the left, to say that φ can be deduced from no premises at all. forall x: Calgary reads A₁, A₂, …, Aₙ ⊢ C as “there is some proof which ends with C” using only those assumptions, and calls a sentence with ⊢ A, provable from nothing, a theorem. A slash through it, ⊬, says no such proof exists. Unicode names the character RIGHT TACK (U+22A2) and gives its other names: turnstile, “proves”, “implies”, “yields”.

Also searched as: ⊢, ⊬, derives symbol, proves symbol, right tack, single turnstile.

⊢ and ⊨

The turnstile has a double-barred partner, ⊨, and the two are easy to mix up. forall x: Calgary insists on the difference: the single turnstile ⊢ concerns the existence of proofs, the double turnstile ⊨ concerns the existence of valuations, that is, ways of making sentences true or false. ⊢ is about what a proof system can derive; ⊨ is about what follows by truth alone. The textbook calls them very different notions, then goes on to show a deep connection between them.

Look-alikes

Unicode has a mirror image, ⊣ LEFT TACK (U+22A3), the reverse turnstile, which it glosses as “non-theorem, does not yield”. The ⊤ and ⊥ are the same strokes turned down and up.