# FOL – Quantifiers and prenex form (from LPL 11.37)

Prenex form – when all the quantifiers are at the front

I am struggling to figure out a couple questions from my book:

``````#7 – ∃x [Cube(x) → ∀x Small(x)]
#8 – ∃x [Cube(x) → ∀x Cube(x)]
``````

I never came accross this before, how can there be quantifiers for the same variable like that? I felt that was strange. But I was working through it this way:

``````1. ∃x [Cube(x) → ∀x Small(x)]
2. ∃x [~Cube(x) v ∀xSmall(x)]
3. ∃x ~~[~Cube(x) v ∀xSmall(x)]
4. ∃x ~[Cube(x) v ~∀xSmall(x)]
5. ∃x ~[Cube(x) v ∃x~Small(x)]
6. ∃x ~∃x[Cube(x) v ~Small(x)]
7. ∃x ∀x[Cube(x) v ~Small(x)]
``````

Now that looks very strange to me and I'm thinking I messed up at part 5-6. I'm guessing that won't work, because there is another variable x before the ∃. But I don't know how else to go about this.

For the second part I got `~∀x Cube(x)`. I don't think that is right either. It would be true if there was anything not an cube in the world, but how can one conclude that there must be no cubes in the world? If they were all cubes, it would also be true.

• @MauroALLEGRANZA Thanks, you answered my question. You should write it as an answer! ;) – zagadka314 Jul 20 '15 at 15:49

The quantifier has a scope : the "inner" ∀x "acts" only on the x in Small(x).

You can "rename" it into ∀y Small(y) and the overall formula still "works", i.e. it does not change its meaning (i.e. its truth-value).

After renaming :

∃x [Cube(x) → ∀y Small(y)]

you can apply the transformation into : ∃x [~Cube(x) v ∀ySmall(y)] and now you can "move inside" the outer quantifier with no harm :

∃x~Cube(x) v ∀ySmall(y).

• Thanks for your answer, I must have missed that in the book somehow. It helps a lot! – zagadka314 Jul 20 '15 at 16:02
• @zagadka313 - see page 323 : "In order to get ready to pull the ∀'s out in front, we replace the x in the second disjunct by a variable (say z) not in the first disjunct". – Mauro ALLEGRANZA Jul 20 '15 at 18:34