Thread: Question about nested quantifiers.

Can someone explain the difference between this:

∀x((x=0)→∃y(xy=1))

.. and this:

∀x∃y((x=0)→(xy=1))

The top one is in my book. The domain is all real numbers. I understand that it's saying that every real number other than zero has a multiplicative inverse, but I don't understand why it can't be written as the second one? Thank you.

You probably mean and not since you write, "every real number other than zero."

The two formulas are equivalent. The second one has an advantage that it is in the prenex normal form. However, the first formula better reflects the meaning of the statement. It guarantees the existence of some y such that xy = 1 only after one provides a proof of . The second formula requires producing some y just on the basis of a given x. In particular, even for x = 0 the interpretation has to provide some y. Later it turns out that this y does not matter because the assumption of the quantifier-free part (matrix) is false, so the matrix is true.

If you consider the two formulas as types of computer programs, the first program takes an x and an evidence that and returns a y and an evidence that xy = 1. The second program takes an x and immediately returns a y such that if later an evidence of is given, then an evidence of xy = 1 is returned. The first program is arguably more reasonable because it returns something only when it has all necessary inputs provided.

However, once again, these are subtleties. In the usual classical logic, both formulas are equivalent.