Mathwords logoMathwords

Turnstile — Definition, Formula & Examples

The turnstile (⊢\vdash) is a symbol in formal logic meaning "proves" or "derives." It states that a conclusion can be reached from a set of premises using the rules of a logical system.

If Γ\Gamma is a set of formulas and φ\varphi is a formula, then Γ⊢φ\Gamma \vdash \varphi asserts that φ\varphi is syntactically derivable from Γ\Gamma within a given formal proof system. When Γ\Gamma is empty, ⊢φ\vdash \varphi means φ\varphi is a theorem of the system.

Key Formula

Γ⊢φ\Gamma \vdash \varphi
Where:
  • Γ\Gamma = A set of premise formulas (may be empty)
  • φ\varphi = The conclusion formula derived from \Gamma
  • ⊢\vdash = The turnstile, read as "proves" or "derives"

How It Works

Place premises on the left side of ⊢\vdash and the conclusion on the right. The statement {A,A→B}⊢B\{A, A \to B\} \vdash B says that BB can be derived from AA and A→BA \to B by applying inference rules (here, modus ponens). The turnstile is purely syntactic: it concerns what you can prove by manipulating symbols, not what is true in a model. Its semantic counterpart is the double turnstile ⊨\models, which asserts that the conclusion is true in every model satisfying the premises.

Example

Problem: Using propositional logic, show that {P, P → Q} ⊢ Q.
Step 1: Assume premise PP.
Step 2: Assume premise P→QP \to Q.
Step 3: Apply modus ponens: from PP and P→QP \to Q, infer QQ.
{P,  P→Q}⊢Q\{P,\; P \to Q\} \vdash Q
Answer: QQ is syntactically derivable from the premises, so {P,P→Q}⊢Q\{P, P \to Q\} \vdash Q holds.

Why It Matters

The turnstile is central to proof theory, automated theorem proving, and programming language type systems. In type theory, the judgment Γ⊢e:τ\Gamma \vdash e : \tau states that expression ee has type τ\tau in context Γ\Gamma, which is the foundation of type-checking in languages like Haskell and OCaml.

Common Mistakes

Mistake: Confusing the single turnstile ⊢\vdash (syntactic derivability) with the double turnstile ⊨\models (semantic entailment).
Correction: ⊢\vdash means "is provable from" using formal rules; ⊨\models means "is true in every model of." They coincide in complete systems (by the completeness theorem), but they are distinct concepts.

Related Terms