You may be operating under several misconceptions. Firstly the notation f: X->Y, putting more space to the right of the colon does occur in mathematical writing (admittedly only 1 of the 3 books I checked used that notation exclusively). Secondly that is still a labelling, you're labelling a map of a specific form (it's almost never used to label anything else, except when dealing with types but that's begging the question).
I suppose it's hard to tell the difference between labelling and stating a property, if I had to give an argument I'd say that you rarely see a formula on the left hand side, except when defining new notations (e.g. let f+g : X -> Y be the map defined by (f+g)(x) = f(x) + g(x)). Compare this to something like 'let x^2 + y^2 = 1' which kind of functions as a labelling (or omits it really) but is really more stating a proposition.
One alternative meaning in mathematics for the colon that does truly differ is using ':' as shorthand for 'such that', though sometimes people use a . or no symbol at all. This is commonly used when defining a set by some proposition e.g. { x : x \in IN and x | 2}, but also sometimes when using quantifiers.
f: X->Y means f maps an input from domain X (set of all real numbers, say) to output range Y (set of all positive real numbers, say, f could be 'abs').
I think you might be thinking it's LX.Y (L for lambda)? But consider X=Y, LX.X is the identity function, some f: X->X could be the identity function, but it could also be anything else that returns a value of the same type as its argument - it could be 'add1' in this example of X being the reals, for example.
I'm not quite sure why this seems to be so controversial, except for the light abuse of notation in my english. Saying that f: X->Y means f maps an input from domain X to output in range Y is to say that we are defining a function -- and labeling it f, since it could just as easily be labeled g and still be the same function. Defining is naming -- naming is labeling [with scope].
It's not defining a function though, it's describing (by one aspect) a whole class of functions.
Take:
f: ints -> ints
f can be 'add1', 'identity', 'double', etc.
If you know that, and calling it 'defining a function' is just loose English (you didn't mean completely defining) then fine, but that's what's confusing people.
It read to me like you thought it was equivalent to a function definition in code, X & Y described what would actually happen over different inputs, so I was just trying to explain, didn't mean to offend if you knew already.
Oooh, I see what you're saying. For want of an "s". Yes, in this context, I am aware that it is a whole class of functions -- and that f is a label being affixed to that class of functions. Sorry for the confusion -- that makes much more sense now.
No offense received -- was just genuinely confused as to why it netted two comments and a few downvotes for a seemingly uncontroversial statement. But then again, we're talking mathematical logic here, so loose english is of course reasonably discouraged.
Thanks for the clarification, and I hope you have a great evening!
I suppose it's hard to tell the difference between labelling and stating a property, if I had to give an argument I'd say that you rarely see a formula on the left hand side, except when defining new notations (e.g. let f+g : X -> Y be the map defined by (f+g)(x) = f(x) + g(x)). Compare this to something like 'let x^2 + y^2 = 1' which kind of functions as a labelling (or omits it really) but is really more stating a proposition.
One alternative meaning in mathematics for the colon that does truly differ is using ':' as shorthand for 'such that', though sometimes people use a . or no symbol at all. This is commonly used when defining a set by some proposition e.g. { x : x \in IN and x | 2}, but also sometimes when using quantifiers.