Introduction

An interesting example for showing how we can automate the reasoning with a language where there are quantifiers, is an algorithm proposed by Mojzesz Presburger in 1929 to decide the validity of a subset of arithmetic.

Language

The language considered by Presburger has the following operators:

the two quantifiers: ∀, ∃ (the set over which we quantify is given by the integers),
the negation (¬),
the implication (⇒),
the equality predicate (=),
the constants 0 and 1,
the sum (+).

For example ∀x. ∃y. (x+y)=0 is a formula of the language under consideration.

Such simple language allows us to also define derived operators:

the conjunction ∧: P ∧ Q is equivalent to ¬(P ⇒ ¬ Q)
the disjunction ∨: P ∨ Q is equivalent to (¬P) ⇒ Q
the scalar product with an integer (.): a.E is equivalent to E + E + .. E, a times
the minus (-): E1 - E2 = E3 is equivalent to E1 = E3 + E2
...

Prenex form

Here, we will consider only the first steps of the Presburger algorithm that aim at reducing any formula into an equivalent one in Prenex DNF. The first operation of the algorithm consists in transforming a formula in such way to have all quantifiers at the beginning of the formula (prenex form). Such a transformation is only valid in the classical logic:

For the negation: ¬(∀x. (P x)) equivalent to ∃x. (¬(P x))
¬(∃x. (P x)) equivalent to ∀x. (¬(P x))

For the implication:: (∀x. (P x)) ⇒ Q equivalent to ∃x. ((P x) ⇒ Q)
(∃x. (P x)) ⇒ Q equivalent to ∀x. ((P x) ⇒ Q)
Q ⇒(∀x. (P x)) equivalent to ∀x. (Q ⇒ (P x))
(Q ⇒ ∃x. (P x)) equivalent to ∃x. (Q ⇒ (P x))

These transformations are valid if there exists no x inside Q that is free. If such x exists, one needs to rename variables suitably. So, ∃x. ((∀x. (P x)) ⇒ (Q x)) is transformed into ∃y. ∃x. ((P x) ⇒ (Q y)) and not in ∃x. ∃x. ((P x) ⇒ (Q x)).

DNF

The second operation of the algorithm is the one that transforms the formula in prenex form into DNF (Disjunctive Normal Form), so to have first the quantifiers, then the disjunctons, then the conjuctions and finally the variables (possibly with negations).

First we expand the implications:: P ⇒ Q equivalent to ¬P ∨ Q

Second, we push down the negations:: ¬(P ∨ Q) equivalent to ¬P ∧ ¬Q
¬(P ∧ Q) equivalent to ¬P ∨ ¬Q
¬(¬P) equivalent to P

Third, we pull the disjunctions before the conjunctions:: P ∧ (Q ∨ R) equivalent to (P ∧ Q) ∨ (P ∧ R)
(Q ∧ R) ∧ P equivalent to (Q ∧ P) ∨ (R ∧ P)

Exercises

*H5. Transform the formula ¬((x∨¬y)⇒z) into DNF.

*H6. Transform the formula ¬((∃x. (P x)) ⇒(∀x. (Q x))) into prenex DNF.

*H7. Transform the formula (∀x.∃y. (P x y)) ⇒(∃x. (P x x)) into prenex DNF.

Monica Nesi