Message Boards Message Boards


Grandfathers/fathers first-order/predicate logic with FindEquationalProof

Posted 16 days ago
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 father

Axiom: A grandfather is the father of a father

Hypothesis: Everyone has a grandfather

FindEquationalProof 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 comments

Regards Uwe

proof = FindEquationalProof[
       grandfather[z, x]]], {ForAll[{x, y, 
        z}, (father[z, y] && father[y, x] \[Implies] grandfather[z, x])],
       ForAll[x, Exists[z, father[z, x]]]}]

enter image description here enter image description here enter image description here

Reply to this discussion
Community posts can be styled and formatted using the Markdown syntax.
Reply Preview
or Discard

Group Abstract Group Abstract