Herbrand Model and Unsat Proof for an Example

We will look at the language ${\cal L} = \{P, R, a, f\}$ where

$P$ is relation symbol of arity one
$R$ is relation symbol of arity two
$a$ is a constant
$f$ is a function symbol of two arguments

Consider this formula in ${\cal L}$ :

$\begin{equation*} \begin{array}{l@{}l} & (\forall x. \exists y.\ R(x,y))\ \land \\ & (\forall x. \forall y.\ R(x,y) \rightarrow \forall z.\ R(x,f(y,z)))\ \land \\ & (\forall x.\ P(x) \lor P(f(x,a)))\ \\ & \rightarrow \forall x. \exists y.\ R(x,y) \land P(y) \end{array} \end{equation*}$

We are interested in checking the validity of this formula (is it true in all interpretations). We will check the satisfiability of the negation of this formula (does it have a model):

$\begin{equation*} \begin{array}{l@{}l} \lnot \bigg( \big( & (\forall x. \exists y.\ R(x,y))\ \land \\ & (\forall x. \forall y.\ R(x,y) \rightarrow \forall z.\ R(x,f(y,z)))\ \land \\ & (\forall x.\ P(x) \lor P(f(x,a)))\ \big)\\ & \rightarrow \forall x. \exists y.\ R(x,y) \land P(y) \bigg) \end{array} \end{equation*}$

Parsing the formula.

Negation normal form.

Skolem normal form for each clause.

Herbrand universe.

Propositional expansion.

Propositional proof.

Recovering first-order proof from propositional proof.