Tautologous Herbrand Expansion

Question

Can someone explain me how to build a herbrand expansion of the following, that is a tautology?

1. $(\exists x) [P(x) \implies (\forall y) P(y)]$
2. $(\exists x) (\forall y) R(x,y) \implies (\forall y)(\exists x) R(x,y)$

My thought's are to bring these formulas into prenex form and than to skolemize them to remove the existential operator. After that i could write the variables as functions, so that i do not have any variable in the sentence...

For the first sentence i tried this:

1. $(\exists x) [P(x) \implies (\forall y) P(y)]$
2. $(\forall y) (\exists x) [P(x) \implies P(y)]$
3. $(\forall y) [P(f(y)) \implies P(y)]$ write x as function of y
4. $[P(f(a)) \implies P(a)]$ with $[x/a]$

But i don't think that this is right. Thank you for your help.

Answer 1

In order to check if a formula is valid (a "FOL tautology") we have to consider its negation.

For the first one [which is valid; see Drinker's Paradox], we have: $\lnot (∃x)[P(x) \to (∀y)P(y)]$.

We start removing $\to$ and moving inside the negation sign, getting:

$(\forall x)[P(x) \land \lnot (∀y)P(y)]$.

Now we considere PNF to get: $(\forall x)P(x) \land \lnot (\forall y)P(y)$, i.e.

$(\forall x)P(x) \land (\exists y) \lnot P(y)$, which is clearly unsatisfiable.

In order to complete the proof using Resolution, we have to consider the two clauses:

$P(x)$ and $\lnot P(a)$,

where we have applied Skolemization:

An existential quantifier that is not preceded by a universal one must be replaced by an individual constant (a $0$-ary function).

Finally, we apply Unification with the substitution $\sigma := [x \leftarrow a]$ and we produce the empty clause, showing that the negated formula is unsatisfiable, i.e. that the original formula is valid.

---

For the second one, we start again considering its negation, and we have two clauses: $(∃x)(∀y)R(x,y)$ and $\lnot (∀y)(∃x)R(x,y)$, i.e.

$(∃x)(∀y)R(x,y)$ and $(∃y)(∀x) \lnot R(x,y)$.

Applying again Skolemization we get: $R(a,y)$ and $\lnot R(x,a)$.

An easy substitution will unify them.

---

---

For details you can see e.g. Mordechai Ben-Ari, Mathematical Logic for Computer Science (Springer, 3rd ed. 2012).