# 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

-

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

-

My answers to your questions would be: (1) Depends on what you mean by "can represent". (2) One doesn't infer logics from other logics. One infers statements from other statements. The Skolem form (a universal formula, which you therefore call equational) of a first-order formula $A$ cannot (in general) be inferred from $A$ in any correct logical system, because it is not (semantically) a consequence of $A$. (3) No; what you call EL is a part of FOPL. (4) Yes; some things provable in FOPL cannot even be formulated in EL. Anything provable in FOPL and statable in EL is provable in EL. – Andreas Blass Apr 22 '11 at 18:18