Find a herbrand model for $\forall x((p(x)\to\lnot p(f(x))) \land (\lnot p (f(f(x)))\to p(f(x))))$

Question

$\forall x((p(x)\to\lnot p(f(x))) \land (\lnot p (f(f(x)))\to p(f(x))))$

So the domain would be the herbrand universe. $p(x)=1 $ iff $x=f(a)$ where $a$ is a constant.

Is what im saying correct ? Would this be a correct herbrand model ?

Answer 1

In this case there is one function symbol $f$. So the Herbrand universe should be the infinite set of syntactic terms $$ \{a, f(a), f(f(a)), f(f(f(a))), \ldots\}. $$ Now, we have to decide what to choose for $p$ in order to make the statement true.

You have suggested that we take $p(f(a)) = \text{true}$ and for all other $x$, $p(x) = \text{false}$. This will satisfy the first part of the statement: $\forall x((p(x)\to\lnot p(f(x)))$. But it will not satisfy the second part, namely $(\lnot p (f(f(x)))\to p(f(x))))$.

• Can you think of an example, why it does not satisfy the second part?

• How can we correct your choice of $p$, so that both the first and second part are true?