A relational symbol indicating semantic entailment or satisfaction between formal structures in logic and model theory.
Examples
Model theory satisfaction
M \models T \text{ means 'M is a model of theory T'}
Logical validity with specific structure
\mathfrak{A} \models \forall x(P(x) \to Q(x))