Combinator logic and unification

Question

Summary: if we are trying to use combinator logic to solve first-order logic type problems, is the best method to feed in free variables and use the standard first-order unification algorithm?

In standard first-order logic, consider the problem of deducing that the following is a contradiction

p(x)
~p(5)

By the rule that we can substitute specific for general, we can derive

p(5)
~p(5)

and q & ~q => false.

The particular choice of the constant 5 to substitute for x is obtained using the standard unification algorithm, which in the case of first-order logic is computable (and indeed quite efficient).

Translating this into combinator logic gives

p = K true
~(p 5)

Substituting the value of p gives

~(K true 5)

Evaluating gives

~true

Which is false, QED.

But it doesn't look so good when we try a more complex expression

p(f(f(x)))
~p(f(f(5)))

In standard first-order logic, unification works just as well here as for the simpler case. The translation to CL, however, is

S (K p) (S (K f) f) = K true
~(p (f (f 5)))

This isn't a problem we can solve with simple substitution. One approach we could try is to feed both sides of an equation the same value; if we take the number 5 as a value, the left-hand side of the equation evaluates as

S (K p) (S (K f) f) 5
K p 5 (S (K f) f 5)
p (S (K f) f 5)
p (S (K f) f 5)
p (K f 5 (f 5))
p (f (f 5))

So we have

p (f (f 5)) = K true 5
p (f (f 5)) = true

Substituting into the second expression from the original problem gives

~true

So we have solved the problem, but we did it by guessing the correct value to feed both sides of the equation, by inspection. Is there a general method that could be used?

One that suggests itself is to feed in a variable, which would give

p (f (f x)) = true

From which the standard first-order unification algorithm could be used.

Have we just established that the only way to solve problems in CL is to convert them back into standard logic? Perhaps it's not that bad; at least we have eliminated lambda and the other quantifiers, and their associated bound variables, leaving only free variables.

Still, is there a better method that I'm missing?

(I'm omitting consideration of types here; because combinator logic is Turing complete, presumably type checking will also be needed to avoid the paradoxes of the sort that make simple untyped lambda calculus unsound.)

Answer 1

I think first-order unification cannot replace higher-order unification because:

(1) if a variable occurs at the predicate position, FO unification is not supposed to handle that, though it may be fixed (seems easy).

(2) more importantly, sometimes a variable can be replaced by a combinatory term containing combinators such as S K I, and upon substitution, the new term may be reduced by combinatory rules to something else, and then becomes identical with the other term. By definition that would be a valid unifier. But FO unification is completely powerless to do that. So HO unification seems much more complex than the FO version...