Translating the following statement in FOL

Question

“A number x is composite (P(x)) if and only if x is divisible by some number y (Q(x, y)) other than 1 or itself, and x is not composite if and only if there does not exist any number y such that y divides x with no remainder.”

This statement can be translated in FOL as the following formula:

           "Ax [P(x) -> (Ey Q(x, y)] & "Ax [~P(x) -> ~Ey (Q(x, y)]

Convert this formula into a normal form showing every step in the process.

Answer 1

1 ∀x [P(x) -> (∃y Q(x, y))] & ∀x [~P(x) -> ~∃y (Q(x, y))]

First, change each of the two implications to the appropriate disjunction using the rule of material implication.

2 ∀x [~P(x) v (∃y Q(x, y))] & ∀x [~~P(x) v ~∃y (Q(x, y))]

Next, eliminate the double-negation

3 ∀x [~P(x) v (∃y Q(x, y))] & ∀x [P(x) v ~∃y (Q(x, y))]

Now convert the existential quantifier in the second disjunct, so as to move the NOT inward

4 ∀x [~P(x) v (∃y Q(x, y))] & ∀x [P(x) v ∀y(~Q(x, y))]

Standardize the variables.

5 ∀x [~P(x) v (∃y Q(x, y))] & ∀x [P(x) v ∀z(~Q(x, z))]

Move all quantifiers outward

6 ∀x∃y[~P(x) v Q(x, y)] & ∀x∀z [P(x) v ~Q(x, z)]

Then

7 ∀x∀z∃y[(~P(x) v Q(x, y)) & [P(x) v ~Q(x, z))]

Skolemize existentially quantified y, replacing it with Skolem function f(x) which maps x to y.

8 ∀x∀z[[~P(x) v Q(x, f(x))] & [P(x) v ~Q(x, z)]]

Finally, drop universal quantifiers

9 [~P(x) v Q(x, f(x))] & [P(x) v ~Q(x, z)]

This translates, roughly speaking, to "Either x is not composite or it is divisible by some f(x) according to the conditions given. And either x is composite or it is not divisible by any z according to the conditions given."