# Prenex and Skolem normal forms

In Mathematica version 7, there was a big advance in logic support ("Boolean computations" is the official name). This was not further developed in version 8.0. So now we have a fairly robust support for propositional calculus, but not too much for predicate calculus.

To this end, it would help a lot if we had an internal function capable of transforming a formula (logic formula, I mean) into the Prenex normal form or, even better, into a Skolem normal form.

Is anybody aware of a 3rd party package which addresses this problem?

• tutorial/RealPolynomialSystems claims "Reduce, Resolve, and FindInstance always put real polynomial systems in the prenex normal form, with quantifier-free parts in the disjunctive normal form"... Jan 20, 2012 at 20:47
• @DanielLichtblau this is a great suggestion Daniel, You may consider putting this as an answer Jan 21, 2012 at 18:53

tutorial/RealPolynomialSystems claims "Reduce, Resolve, and FindInstance always put real polynomial systems in the prenex normal form, with quantifier-free parts in the disjunctive normal form..."

For obtaining Skolem form from prenex, possibly could proceed as described at

http://demonstrations.wolfram.com/Skolemization/

or

http://mathworld.wolfram.com/SkolemFunction.html

Edit:

Also there is a non-System context function of interest (I learned this via grep). I'll illustrate with the example provided in a comment.

ee = ForAll[x, P[x] \[Implies] Q[x]] \[Implies] (ForAll[x, P[x]] \[Implies] ForAll[x, Q[x]]);


We'll need to put into a normal for; conjunctive or disjunctive will suffice. I'll use LogicalExpand to get a dnf.

ff = LogicalExpand[ee]

Exists[x,  !Implies[P[x], Q[x]]] || Exists[x,  !P[x]] || ForAll[x, Q[x]]

ReduceToPrenexForm[ff]

Exists[{C[1], C[2]}, ForAll[{C[3]}, (P[C[1]] &&  !Q[C[1]]) ||  !P[C[2]] || Q[C[3]]]]


I've no idea whether this is the sort of result wanted. But it does seem to have all quantifiers at the front.

• As I said above this is an excellent suggestion, but it does not really solve my problem. It seems that this transformation to prenex normal form, which takes place internally (probably with Resolve), is executed only on polynomial systems, not general first-order language formulas. For ex: ForAll[x, P[x] [Implies] Q[x]] [Implies] (ForAll[x, P[x]] [Implies] ForAll[x, Q[x]]) // Resolve does not do anything, because the expr is not in the form expected by MMA. Is there some undocumented function which can deal with this more general situation? Jan 24, 2012 at 1:43
• @magma See edited post. Jan 24, 2012 at 16:46
• Great Daniel! This is exactly the result I was looking for. I do not understand why WRI keeps this function undocumented. It is very useful in ATP. But this will be the topic for another question Jan 24, 2012 at 17:09
• @magma It turns out we don't document this because prenex repositioning and skolemization are illegal activities in most southern states. (Did I really write that?) Jan 27, 2012 at 23:26
• @Magma Yes, I agree maybe that remark was a bit too cryptic. What I meant was that, having access to the source files (and working on a Linux desktop), I used grep on them to learn that a ToPrenexForm function existed. I do not know if this would work with the .mx files that come with the Mathematica distribution (I do not know the extent to which things might be encrypted therein; possibly not at all). Jan 31, 2012 at 17:18