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.)