FOPL and equational logic

Question

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

Answer 1

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

Answer 2

Thanks for your helpful response. I am trying to understand your comment:

"Skolem form of a sentence implies the original sentence but is not in general a logical consequence of it."

Does this mean any of the following: 1) That the Skolem form of EL can represent FOPL (sentences). 2) The Skolem form of EL cannot be logically inferred from FOPL (in what logic FOPL or EL? I assume FOPL). 3) Things provable in EL may not be provable in FOPL. 4) Things provable in FOPL may not be provable in EL.

Thanks, Pat