Hard Predicate Proof Help

Question

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

Answer 1

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.

Answer 2

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.