1. ## Confused about quantitfiers and such

Is there a difference between ∀X (odd(X) => (∃Y (X = 2 x Y ))) and ∀X ∃Y (odd(X) => (X = 2 x Y ))?

The first one seems off, but I can't say why. Or do they both mean the same thing?

2. Originally Posted by owq
Is there a difference between ∀X (odd(X) => (∃Y (X = 2 x Y ))) and ∀X ∃Y (odd(X) => (X = 2 x Y ))?

The first one seems off, but I can't say why. Or do they both mean the same thing?
i would translate into english.

for all x, if x is odd then there exists a y such that x is twice y. (false in integers, true in reals)

for all x, there exists a y such that if x is odd then x is twice y. (false in integers, true in reals)

(Note: Some errors beyond this point, see further posts for details.)

they are semantically distinct, but in this case they happen to be logically equivalent (have the same truth value). perhaps more illuminating is an example where one is true and one is false.

∀X (X^2=1 => (∃Y in {-1,1} (X=Y)))

versus

∀X ∃Y in {-1,1} (X^2=1 => (X=Y))

compare to the example here, see in particular MattMan's response

http://www.mathhelpforum.com/math-he...ts-150433.html

and actually i just found a relevant passage on wikipedia that gives the exact same example

Quantification - Wikipedia, the free encyclopedia

3. Your second expression is just the first converted to prenex normal form.

4. Originally Posted by Ackbeet
Your second expression is just the first converted to prenex normal form.
What about my example with X^2=1? Did I make a mistake?

Additional info: The "in {-1,1}" part is optional; the main difference is that Y is no longer unique in the example I gave.

5. I was referring to the OP in post # 3. Sorry if I introduced confusion there.

they are semantically distinct, but in this case they happen to be logically equivalent
I wouldn't say they happen to be logically equivalent. If one is the prenex form of the other, they will always be logically equivalent, right?

Your example is an example of converting to prenex normal form. I don't think it changes the truth value of the statement. Converting your first example to prenex normal form gives you

(∀X) (∃Y in {-1,1}) (X^2=1 => ( X=Y ))

(∀X) (∃Y in {-1,1}) (X^2=1 => ( X=Y )).

So you can see that these expressions are really the same, and I'd say they're both true.

Does that make sense? So I'm not sure I would say you "made a mistake"; rather, I'm just not sure you're addressing what the OP'er asked. Your English translations are correct, and very helpful, I think.

6. Originally Posted by Ackbeet
I was referring to the OP in post # 3. Sorry if I introduced confusion there.
I saw you were referring to the OP, no confusion there.

Originally Posted by Ackbeet
I wouldn't say they happen to be logically equivalent. If one is the prenex form of the other, they will always be logically equivalent, right?

Your example is an example of converting to prenex normal form. I don't think it changes the truth value of the statement. Converting your first example to prenex normal form gives you

(∀X) (∃Y in {-1,1}) (X^2=1 => ( X=Y ))

(∀X) (∃Y in {-1,1}) (X^2=1 => ( X=Y )).

So you can see that these expressions are really the same, and I'd say they're both true.

Does that make sense? So I'm not sure I would say you "made a mistake"; rather, I'm just not sure you're addressing what the OP'er asked. Your English translations are correct, and very helpful, I think.
Thanks a lot for the reply but I don't think

(∀X) (∃Y in {-1,1}) (X^2=1 => ( X=Y ))

is true. The two statements

X^2=1 => X=1

and

X^2=1 => X=-1

are both false, even though their converses are true. Thus there does not exist a Y such that X^2=1 => X=Y. Right?

7. I think I haven't been careful enough here. Putting the $y$ in the set $\{-1,1\}$ may have to be dissociated from the $y$ quantifier. Let me see here: we all agree that

$(\forall x) ((x^{2}=1) \to (\exists y \in \{-1,1\}) (x=y))$

is true. Let me dissociate the $y$ quantifier from the set inclusion property:

$(\forall x) ((x^{2}=1) \to (\exists y)((y \in \{-1,1\}) \land(x=y))).$

You'd agree I haven't changed anything? Now the rules for removing quantifiers from implications say that I can remove a quantifier from the consequent without changing anything. So I can do this:

$(\forall x)(\exists y) ((x^{2}=1) \to ((y \in \{-1,1\}) \land(x=y))).$

This is now in prenex normal form, and must still be true. Would you agree?

I think this might be what you're getting at with your statement

Y is no longer unique in the example I gave.
Now, getting back to the OP: because there is no hidden term tacked on to either quantifier, I'd say that both forms are logically the same because one is just the prenex form of the other. They're both false if Y must be an integer, and they're both true if Y is allowed to be a rational number.

Hopefully this clears things up a bit.

8. I realized while on an errand that I confused

(∀X) (∃Y in {-1,1}) (X^2=1 => ( X=Y ))

with

(∃Y in {-1,1}) (∀X) (X^2=1 => ( X=Y ))

So I definitely made a mistake! Thanks for bearing with me, sorry for that.

9. Ah, I see. Yeah, you definitely can't switch the order of mixed quantifiers.

10. A deep question and a nice discussion. I agree with Ackbeet.

$(\forall x)(\exists y) ((x^{2}=1) \to ((y \in \{-1,1\}) \land(x=y)))$
Of course, this proposition is true. Indeed, suppose x is given. If x = 1, there exists a y = 1. If x = -1, then take y = -1. Finally, if x is neither 1 nor -1, take any y from {1, -1}: the premise $x^2=1$ is false; so the value of y does not matter. Also, it is not necessary to break $\exists y\in\{1, -1\}.\,x=y$ into $\exists y.\,y\in\{1,-1\}\land x=y$; both formulas are true. And yes, the formula above is the prenex normal form of

$(\forall x) ((x^{2}=1) \to (\exists y \in \{-1,1\}) (x=y))$

so they are equivalent.

And yet,

$\forall x.\,A(x)\to\exists y.\,B(x,y)$ (1)

and

$\forall x\exists y.\,A(x)\to B(x,y)$ (2)

are not 100% equivalent. (2) always implies (1), but two things are needed for the converse. First, the domain that y range over must be nonempty; otherwise, (1) is true if A(x) is always false, but (2) is false. Second, one needs the law of excluded middle applied to A(x). Indeed, suppose we are proving (2) and x is given. If A(x) is true, then, using (1), we have $\exists y.\,B(x,y)$, so we have y and a proof of B(x,y), as required. If A(x) is false, then take any y since the premise of the rest of (2) is false. In regular logic courses, both of the conditions above are assumed.

From the programmer's viewpoint, however, (1) and (2) are types of functions that take x and a proof of A(x) and return y and a proof of B(x,y). Then it matters whether a function takes two arguments: x and a proof of A(x), or just one: x, before returning y. One may not be able to test whether A(x) is true (this almost always happens in practice), so when one is given a proof of A(x), this is an extra piece of information that may be crucial in computing y.