# Grandfathers/fathers first-order/predicate logic with FindEquationalProof

Posted 16 days ago
250 Views
|
0 Replies
|
1 Total Likes
|
 I tried my first simple proof in first-order/predicate logic with FindEquationalProof (12.3) and the following example:Axiom: Everyone has a fatherAxiom: A grandfather is the father of a fatherHypothesis: Everyone has a grandfatherFindEquationalProof finds a proof within 22 steps, but some intermediate steps seem to be logically not correct: In the EquationalizedHypothesis the Exists-quantifier is substituted by a Skolem-function f1. But in the EquationalAxiom5 from the same form of Axiom2, the Exists-quantifier is substituted only by father [x3,x1] without a Skolem-function. This finally leads to strange propositions like: father[x0,x0]==grandfather[x3,x1] which are logically invalid.I guess this proof is not really a valid proof. Would someone help me with some hints, what is going wrong here ? Thank you for any commentsRegards Uwe proof = FindEquationalProof[ ForAll[x, Exists[z, grandfather[z, x]]], {ForAll[{x, y, z}, (father[z, y] && father[y, x] \[Implies] grandfather[z, x])], ForAll[x, Exists[z, father[z, x]]]}]