TeXipedia

vDash

Represents a double vertical bar followed by a horizontal dash, commonly used in mathematical logic to denote semantic entailment or model-theoretic consequence.

Overview

Essential in formal logic and mathematical proofs where precise notation for semantic relationships between statements is required.

  • Frequently used in model theory to indicate that a structure satisfies a formula or theory
  • Common in proof theory and mathematical logic textbooks
  • Distinguished from similar symbols like \vdash (syntactic consequence) by indicating semantic rather than syntactic relationships
  • Often appears in formal specifications and theoretical computer science when describing logical properties

Examples

Expressing logical consequence in formal logic, showing that a conclusion follows from premises.

P∧Q⊨RP \land Q \vDash R 
P \land Q \vDash R

Showing semantic entailment in mathematical logic, where multiple premises entail a conclusion.

(P→Q),(Q→R)⊨P→R(P \to Q), (Q \to R) \vDash P \to R 
(P \to Q), (Q \to R) \vDash P \to R

Demonstrating model-theoretic satisfaction in formal semantics.

M⊨ϕ\mathcal{M} \vDash \phi 
\mathcal{M} \vDash \phi