# Hard Predicate Proof Help

I have been working on this proof for over a week now, and I can't seem to figure it out:

Pd ⟷ (Hj & Mj), Gsd, ∀x∀y∃z(((Gxy & (Py ➝ Pz)) & Rxyz) ➝ Gxz), Pe ⟷ ∀x(Hx ➝ Mx), Rsde |- Gse

I am stuck with figuring out what to do with the existential quantifier in the third premise. Does anyone have any tips on basic strategies for this proof?

Best, Justin

• On what ground do you think that it is provable ? May 29 '19 at 19:16

This is not provable. Consider the following model with the domain {d,e,i,j,s}:

• P = {d}
• H = {i, j}
• M = {j}
• G = {<s,d>}
• R = {<s,d,e>}

We get:

• Pd ⟷ (Hj & Mj) is true, because both sides are true.
• Gsd is true.
• ∀x∀y∃z(((Gxy & (Py ➝ Pz)) & Rxyz) ➝ Gxz) is true, because the antecedent is false for any z.
• Pe ⟷ ∀x(Hx ➝ Mx) is true, because both sides are false.
• Rsde is true.
• Gse is false.

So in this model each premise is true and the conclusion is false. So the conclusion doesn't follow from the premises.

I am stuck with figuring out what to do with the existential quantifier in the third premise.

Let us have a quick look. You are aiming to derive `Gse` from the premises, so first use universal elimination on the third, and then...

`````` | Pd ⟷ (Hj & Mj)
| Gsd
| ∀x∀y∃z(((Gxy & (Py ➝ Pz)) & Rxyz) ➝ Gxz)
| Pe ⟷ ∀x(Hx ➝ Mx)
| Rsde
|-
| ∀y∃z(((Gsy & (Py ➝ Pz)) & Rsyz) ➝ Gsz)
| ∃z(((Gsd & (Pd ➝ Pz)) & Rsdz) ➝ Gsz)
``````

… Nope, you cannot do anything else. You cannot establish that term `e` is a witness for that existential, and further you cannot derive that `Pd ➝ Pe` . You have no route to deriving `Gse` ; it simply is not entailed by these premises.