# Prenex form and quantifiers (from LPL 11.37)

i'm trying to solve the exercise 11.37 from LPL textbook (Logic Proof and Logic) and I'm blocked. I had to write a prenex normal form of each sentence. I tried a lot of times to do these two sentences:

¬∃x[Cube(x) ∧ ∀y (Tet(y) → ∃z Between(z, x, y))]


and

∃x Cube(x) ↔ ∀x Small(x)


Any suggestions? Thanks.

• I must write the prenex normal form of each sentence, sorry. – Alessandro Lunardi Dec 27 '17 at 20:34

Here's what I came up with:

~Ǝx[Cx & ∀y[Ty → Ǝz[Bzxy]]]
∀x[Cx → ~∀y[Ty → Ǝz[Bzxy]]]
∀x[Cx → ~∀y[Ǝz[Ty → Bzxy]]]
∀x[Cx → Ǝy[∀z[~(Ty → Bzxy)]]]
∀x[Ǝy[Cx → ∀z[~(Ty → Bzxy)]]]
∀x[Ǝy[∀z[Cx → ~(Ty → Bzxy)]]]
∀x[Ǝy[∀z[Cx → ~(~Ty ∨ Bzxy)]]]
∀x[Ǝy[∀z[Cx → (Ty & ~Bzxy)]]]


And the second one:

Ǝx[Cx] ⇔ ∀x[Sx]
(Ǝx[Cx] → ∀x[Sx]) & (∀x[Sx] → Ǝx[Cx]) rename
(Ǝx[Cx] → ∀y[Sy]) & (∀z[Sz] → Ǝw[Cw])
(∀x[Cx → ∀y[Sy]]) & (Ǝz[Sz → Ǝw[Cw]])
∀x[∀y[Cx → Sy] & Ǝz[Ǝw[Sz → Cw]]]
∀x[∀y[(Cx → Sy) & Ǝz[Ǝw[Sz → Cw]]]]
∀x[∀y[Ǝz[Ǝw[(Sz → Cw) & (Cx → Sy)]]]]


The first exercise could be transformed in the following way:
1. ¬∃x [Cube(x) ∧ ∀y (Tet(y) → ∃z Between(z,x,y))]
2. ∀x ¬[Cube(x) ∧ ∀y (Tet(y) → ∃z Between(z,x,y))] - De Morgan's law for quantifiers
3. ∀x [¬Cube(x) ∨ ¬∀y (Tet(y) → ∃z Between(z,x,y))] - De Morgan's law for propositional logic
4. ∀x [¬Cube(x) ∨ ∃y ¬(Tet(y) → ∃z Between(z,x,y))] - De Morgan's law for quantifiers
5. ∀x [¬Cube(x) ∨ ∃y ¬(¬Tet(y) ∨ ∃z Between(z,x,y))]- replace implication
6. ∀x∃y [¬Cube(x) ∨ ¬(¬Tet(y) ∨ ∃z Between(z,x,y))] - pull out y-variable applying null quantification principle
7. ∀x∃y [¬Cube(x) ∨ (¬¬Tet(y) ∧ ¬∃z Between(z,x,y))] - inject negation into the parenthesis using De Morgan's law for propositional logic
8. ∀x∃y [¬Cube(x) ∨ (Tet(y) ∧ ¬∃z Between(z,x,y))] - cancel double negation in front of Tet(y) using negation elimination rule
9. ∀x∃y [¬Cube(x) ∨ (Tet(y) ∧ ∀z ¬Between(z,x,y))] - De Morgan's law for quantifiers
10. ∀x∃y∀z [¬Cube(x) ∨ (Tet(y) ∧ ¬Between(z,x,y))] - null quantification principle for z-variable
11. ∀x∃y∀z [Cube(x) → (Tet(y) ∧ ¬Between(z,x,y))] - replace disjunction by implication ∎

• It seems like more is needed here. What I think you have is ¬∃x[Cube]. – Frank Hubeny Jan 27 at 22:14