MathOverflow is a question and answer site for professional mathematicians. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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

share|cite|improve this question

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

share|cite|improve this answer

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

share|cite|improve this answer
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

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.