Logical consequence

Summary

A formula $\varphi$ is a logical consequence of a set of formulas $\Gamma$ when every interpretation making all of $\Gamma$ true makes $\varphi$ true. This is written $\Gamma \models \varphi$. It is the semantic notion of "follows from", in contrast with derivability $\Gamma \vdash \varphi$ in a proof system. Soundness and Gödel's completeness theorem say that the two notions agree in first-order logic.