Formules, variables libres

Les formules atomiques sont les mots $= t_1\, t_2$ et $R\, t_1 \cdots t_n$, où $R$ est un symbole de relation d'arité $n$ et les $t_i$ des termes. Les formules forment le plus petit ensemble de mots contenant les formules atomiques et stable par $\varphi \mapsto \neg\varphi$, $(\varphi, \psi) \mapsto\, \to \varphi\, \psi$ et $\varphi \mapsto \forall x\, \varphi$.

Une occurrence d'un symbole dans un mot est une place où il figure. Pour une variable $x$, on ne compte pas la lettre $x$ qui suit immédiatement un symbole $\forall$ : elle fait partie du bloc $\forall x$. Une sous-formule d'une formule $\varphi$ est une formule formée de symboles consécutifs de $\varphi$.

Dans $\forall x\, \psi$, la formule $\psi$ est la portée du quantificateur. Une occurrence de $x$ est liée si elle se trouve dans la portée d'un quantificateur $\forall x$, et libre sinon. Une formule sans variable libre est un énoncé, ou formule close, et un ensemble d'énoncés est une théorie.

La clôture universelle d'une formule $\psi$ dont les variables libres sont $x_{i_1}, \dots, x_{i_g}$, avec $i_1 < \cdots < i_g$, est la formule $\forall x_{i_1} \cdots \forall x_{i_g}\, \psi$. C'est un énoncé : une occurrence libre de $x_{i_m}$ dans $\psi$ se trouve dans la portée du quantificateur $\forall x_{i_m}$, qui contient $\psi$, et une occurrence liée dans $\psi$ le reste.