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
Your second expression is just the first converted to prenex normal form.
I was referring to the OP in post # 3. Sorry if I introduced confusion there.
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?they are semantically distinct, but in this case they happen to be logically equivalent
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 ))
Your second expression was already in prenex normal form:
(∀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.
I saw you were referring to the OP, no confusion there.
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?
I think I haven't been careful enough here. Putting the in the set may have to be dissociated from the quantifier. Let me see here: we all agree that
is true. Let me dissociate the quantifier from the set inclusion property:
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:
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
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.Y is no longer unique in the example I gave.
Hopefully this clears things up a bit.
A deep question and a nice discussion. I agree with Ackbeet.
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 is false; so the value of y does not matter. Also, it is not necessary to break into ; both formulas are true. And yes, the formula above is the prenex normal form of
so they are equivalent.
And yet,
(1)
and
(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 , 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.