Search code examples
logicpredicate

In predicate logic, why does P(x) and P(f(x)) have no unifiers?

In predicate logic, why does P(x) and P(f(x)) have no unifiers? One of my solutions is replacing x with f(x), but I'm not sure why I am wrong.

Solution

  • Let's see what happens if you replace x with f(x):

    • P(x) becomes P(f(x))
    • P(f(x)) becomes P(f(f(x)))

    And the result isn't the same; so it's not a unifier.

    In general when the difference term involves itself as in this case (i.e., x differing from f(x)) you cannot unify them since whatever you substitute for x would change both terms in an unequal way, assuming they are not equal to start with.

    Another way to think about this the so called occurs-check. Since x occurs in f(x) you cannot unify these two terms. You can read about the occurs-check here: https://en.wikipedia.org/wiki/Occurs_check