The formulae $F$ and $G$ are called (semantically) equivalent, if for all interpretations ${\mathcal {I}}$ for $F$ and $G$, ${\mathcal {I}}(F)={\mathcal {I}}(G)$. We write $F\equiv G$.
The equivalences from the propositional case in theorem 4 equivalences hold and in addition we have the following cases for quantifiers.
with $x$ has no free occurrence in $G$, as an example. Assume an interpretation ${\mathcal {I}}=(U,{\mathcal {A}})$ such that
${\mathcal {I}}(\forall xF\land G)=true$
${\text{iff }}{\mathcal {I}}(\forall xF)=true{\text{ and }}{\mathcal {I}}(G)=true$
${\text{iff }}{\text{ for all }}d\in U:{\mathcal {I}}_{[x/d]}(F)=true{\text{ and }}{\mathcal {I}}(G)=true$
${\text{iff }}{\text{ for all }}d\in U:{\mathcal {I}}_{[x/d]}(F)=true{\text{ and }}{\mathcal {I}}_{[x/d]}(G)=true{\text{ (x = does not occur free in = G)}}$
${\text{iff }}{\text{ for all }}d\in U:{\mathcal {I}}_{[x/d]}((F\land G))=true$
Let $F$ be a formula, $x$ a variable and $t$ a term. $F[x/t]$ is obtained from $F$ by substituting every free occurrence of $x$ by $t$.
Note, that this notion can be iterated: $F[x/t_{1}][y/t_{2}]$ and that $t_{1}$ may contain free occurrences of $y$.
A formula is called in prenex form if it has the form $Q_{1}\cdots Q_{n}F$, where $Q_{i}\in \{\forall ,\exists \}$ with no occurrences of a quantifier in $F$
where ${\overline {Q_{i}}}={\begin{cases}\;\;\,\exists &ifQ_{i}=\forall \\\;\;\,\forall &ifQ_{i}=\exists \end{cases}}$
$F=F_{1}\circ F_{2}$ with $\circ \in \{\land ,\lor \}$. There exists $G_{1},G_{2}$ which are proper and in prenex form and $G_{1}\equiv F_{1}$ and $G_{2}\equiv F_{2}$. With bounded renaming we can construct
where $f$ is a new function symbol. We have to prove that this transformation is satisfiability preserving: Assume $F'$ is satisfiable. than there exists a model ${\mathcal {I}}$ for $F'$${\mathcal {I}}$ is an interpretation for $F$. From the model property we have for all $u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}$
where $v={\mathcal {I}}(f(u_{1},\cdots ,u_{n})$. Hence we have, that for all $u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}$ there is a $v\in U_{\mathcal {I}}$, where
and hence we have, that ${\mathcal {I}}(\forall y_{1}\cdots \forall y_{n}\exists z\;G)=true$, which means, that ${\mathcal {I}}$ is a model for $F$.
For the opposite direction of the theorem, assume that $F$ has a model ${\mathcal {I}}$. Then we have, that for all $u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}$, there is a $v\in U_{\mathcal {I}}$, where
Let ${\mathcal {I'}}$ be an interpretation, which deviates from ${\mathcal {I}}$ only, by the fact that it is defined for the function symbol $f$, where ${\mathcal {I}}$ is not defined. We assume that $f^{{\mathcal {I}}'}(u_{1},\cdots ,u_{n})=v$, where $v$ is chosen according to the above equation.
Hence we have that for all $u_{1},\cdots ,u_{n}\in U_{\mathcal {I}}'$
which means, that ${\mathcal {I}}'(\forall y_{1}\cdots \forall y_{n}\;G[z/f(y_{1},\cdots ,y_{n})])=true$, and hence ${\mathcal {I}}'$ is a model for $F'$.
The above results can be used to transform a Formula into a set of clauses, its clause normal form:
Transformation into Clause Normal Form
Given a first order formula $F$.
Transform $F$ into an equivalent proper $F_{1}$ by bounded renaming.
Let $y_{1},\cdots ,y_{k}$ the free variables from $F_{1}$. Transform $F_{1}$ into $F_{2}=\exists y_{1}\cdots \exists y_{k}\;F_{1}$
Transform $F_{2}$ into an equivalent prenex form $F_{3}$.
Transform $F_{3}$ into its Skolemform $F_{4}=\forall x_{1}\cdots \forall x_{l}\;G$
Transform $G$ into its CNF $G\prime =(\bigwedge _{i=1}^{n}~(\bigvee _{j=1}^{m}~L_{i,j}))$ where $L_{ij}$ is a literal. This results in $F_{5}=\forall x_{1}\cdots \forall x_{l}\;G\prime$
Let $F$ be a formula, $x$ a variable and $t$ a term. Then $F[x/t]$ denotes the formula which results from $F$ by replacing every free occurrence of $x$ by $t$. Give a formal definition of this three argument function $F[x/t]$, by induction over the structure of the formula $F$.