theory

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

We write $T\models \varphi$ for any formula $\varphi$ if every model $ℳ$ of $ℒ$ such that $M\models T$, $M\models \varphi$.

We write $T⊢\varphi$ is for there is a proof of $\varphi$ 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$:

$$\{\phi \mid S\vDash \phi \},$$

and is denoted by $\mathrm{Th}(S)$.