stylistic:style_transfer
Validity, satisfiability, and logical consequence

If a sentence φ evaluates to true under a given interpretation M, one says that M satisfies φ; this is denoted M ⊨ φ {\displaystyle M\vDash \varphi }. A sentence is satisfiable if there is some interpretation under which it is true. This is a bit different from the symbol ⊨ {\displaystyle \vDash } from model theory, where M ⊨ ϕ {\displaystyle M\vDash \phi } denotes satisfiability in a model, i.e. "there is a suitable assignment of values in M {\displaystyle M} 's domain to variable symbols of ϕ {\displaystyle \phi } ".

Satisfiability of formulas with free variables is more complicated, because an interpretation on its own does not determine the truth value of such a formula. The most common convention is that a formula φ with free variables x 1 {\displaystyle x_{1}},..., x n {\displaystyle x_{n}} is said to be satisfied by an interpretation if the formula φ remains true regardless which individuals from the domain of discourse are assigned to its free variables x 1 {\displaystyle x_{1}},..., x n {\displaystyle x_{n}}. This has the same effect as saying that a formula φ is satisfied if and only if its universal closure ∀ x 1 … ∀ x n ϕ (x 1, …, x n) {\displaystyle \forall x_{1}\dots \forall x_{n}\phi (x_{1},\dots,x_{n})} is satisfied.

A formula is logically valid (or simply valid) if it is true in every interpretation. These formulas play a role similar to tautologies in propositional logic.

A formula φ is a logical consequence of a formula ψ if every interpretation that makes ψ true also makes φ true. In this case one says that φ is logically implied by ψ.