∀x(Fx → ∀y(Fy → y=x))

Hello!

This is pretty much my first venture in to this notation, and I was wondering if someone could help me with this:

∀x(Fx → ∀y(Fy → y=x))

As far as I am aware, ∀y(Fy → y=x) means for all y, whatever y you plug in, its domain is limited to x, so y is x, and f(y) is f(x): i.e. it limits y to 'being' x.
Something like (Fx & ∀y(Fy → y=x)) makes sense, because its basically saying F can only be over x: there is only one F, namely x; if we tried to introduce something else, ∀y(Fy → y=x) tells us that it has to be x, so it can't be anything else, only x.

If ∀y(Fy → y=x) = u

then what does ∀x(Fx → u) mean? There's no u = x, is it over a domain?, or is it saying if F(x) is true then u? In which case the same notation is saying different things, which apparently it can; but in this case without clarification that this is is happening.
Or is it saying something like: for all x: for F(x), y in F(y) is limited to being x, and that this is true for all y?

Hopefully that makes sense.
Any help appreciated!

 

Thanks for the responses.

Here it is in 'context':

∃x(Fx [itex]\wedge[/itex] ∀y(Fy → y=x) & Bx)

So looking at this component, two requirements are made on x:

Fx [itex]\wedge[/itex] ∀y(Fy → y=x)

The ∀y(Fy → y=x) component was the one we were addressing. I meant to say maps the domain of y onto the codomain x; but thinking about it, this doesn't make sense here, as you are not mapping y on to x; and the notation is not quite the same, although similar. It doesn't appear to be a Boolean valued function either, even though the notation again looks similar. What does the arrow denote here, exactly? What is it called?

So if you can plug in some y, which doesn't equal x, then ∀y(Fy → y=x) is not true and therefore the requirements that some x meets Fx [itex]\wedge[/itex] ∀y(Fy → y=x) is not fulfilled; so the whole statement is false?

This would mean my understanding of what something like ∃x(Fx [itex]\wedge[/itex] ∀y(Fy → y=x) & Bx) is saying is false. I understood it to be stating something unchanging, that ∀y(Fy → y=x) 'states' that there is a unique F(x); instead, it appears as a function that can change and can be render the statement ∃x(Fx [itex]\wedge[/itex] ∀y(Fy → y=x) & Bx) true or false.
Do you see what I mean?:
In one understanding, my initial one, ∃x(Fx [itex]\wedge[/itex] ∀y(Fy → y=x) & Bx) says that there is some x such that it is uniquely F(x) becuase ∀y(Fy → y=x) means any y has to be x, so that F is limited to being x (i.e. it is unique).
In the second understanding, you are saying that a y can be plugged in that does not equal x, and so it renders the 'dynamic' statement ∃x(Fx [itex]\wedge[/itex] ∀y(Fy → y=x) & Bx) false because ∀y(Fy → y=x) is false. This is subtly different; since, although it restricts the values of y to x in order to render it true, it is a slightly different statement - a kind of dynamic statement. It's no longer saying explicitly that F(x) is unique, but says that, if y isn't equal to x, then the statement is false. Does that make sense? Admittedly, it seems to amount to the same thing, but I think there is a conceptual difference. In the second case its more dynamic; as you say, it can accept values for y not equal to x; rendering the statement false, but acceptable none the less. In the first it is saying you cannot even plug in values of y not equal to x, since they have to equal x.

Any further help appreciated.