Q:

FOPL and equational logic

Hi,
I am trying to convert First Order Predicate Logic (FOPL) sentences to sentences in Equational Logic (EL). I am using Skolem constants and function to represent FOPL existential quantification in the EL sentences. Here is an example of defining overlap in terms of the part-of relation:
-- FOPL definition of overlap \A denotes for all, \E denotes there exists
ax [A9] : \A[x:Entity, y:Entity] \E[z:Entity] overlap(x, y) = (part-of(z, x) & part-of(z, y))  
-- Equational logic (EL) definition of overlap
-- In EL variables are univerally quantified, exestential quantification is simulated by Skolem function f.
vars  x y z : Entity
eq [A9] :  overlap(x, y) = (part-of(f(y), x) and part-of(f(x), y)) 
I have two questions:
1) Is the above translation valid?
2) Using this technique is it in general possible to represent FOPL sentences in EL.
Thanks,
Pat

A:

This question seems confused in several respects.  First, a minor point, "equational logic" ordinarily means that no predicates except equality are available; your equational translation, however, uses the "overlap" and "part-of" relations.  
Second, if your definition of "overlap" is to give the usual meaning, then \Ez should apply to the right side of your equation (which is really an "if and only if" since the two sides are formulas), not to the whole equation.  
Perhaps more important is that, when one Skolemizes a formula, an existentially quantified variable (z in your example) should be replaced by a Skolem function with, as its arguments, all the universally quantified variables in whose scope the relevant existential quantifier lies.  So in your example, z would be replaced by f(x,y) (at both occurrences), not by f(y) at one occurrence and f(x) at the other.  
Finally, the Skolem form of a sentence implies the original sentence but is not in general a logical consequence of it.  What would be equivalent to the original sentence would be a second-order form of the Skolemization where, after replacing existential variables by Skolem functions (with the appropriate arguments), you existentially quantify over all the Skolem functions.  
(Technical caution: I've written "existentially" quantified variables to mean "quantifiers that would become existential in prenex form"; dually for "universal".)

