If $L$ is a logical language for some logic $\mathcal{L}$ , a set $T$ of formulas with no free variables is called a theory (of $\mathcal{L}$ ). If $\mathcal{L}$ is a first-order logic, then $T$ is called a first-order theory.

We write $T\vDash \phi$ for any formula $\phi$ if every model $\mathcal{M}$ of $\mathcal{L}$ such that $M\vDash T$ , $M\vDash\phi$ .

We write $T\vdash\phi$ is for there is a proof of $\phi$ from $T$ .

Remark. Let $S$ be an $L$ -structure for some signature $L$ . The theory of $S$ is the set of formulas satisfied by $S$ : $$\lbrace \varphi \mid S\models \varphi \rbrace,$$ and is denoted by $\operatorname{Th}(S)$ .