Formulas (Predicate Logic)

Given a vocabulary $\sigma$, the $\sigma$-formulas of a first-order language over $\sigma$ are expressions from $A_{\sigma }^{\ast }$ defined by the following rules:

• $\top$ and $\perp$ are $\sigma$-formulas
• if $t_1$ and $t_2$ are $\sigma$-terms, then $t_1=t_2$ is also a $\sigma$-formula (an atomic formula)
• if $t_1,...,t_n$ are $\sigma$-terms and $P$ is an $n$-ary predicate in $\sigma$, then the atom $P(t_1,...,t_n)$ is also a $\sigma$-formula (also an atomic formula)
• if $\varphi$ is a $\sigma$-formula, then $\neg (\varphi )$ is also a $\sigma$-formula
• if $\varphi$ and $\phi$ are $\sigma$-formulas, then $(\varphi \wedge \phi ),(\varphi \vee \phi ),(\varphi \to \phi ),\text{ and }(\varphi \leftrightarrow \phi )$ are also $\sigma$-formulas
• if $x$ is a variable and $\varphi$ is a $\sigma$-formula $(\exists x)(\varphi )$ and $(\forall x)(\varphi )$ are also $\sigma$-formulas