Talk:Function application

Relation application

Application can be of relations in general; function application is a special case for when the relation is functional. Can something be mentioned about this? I don't know whether anyone has used the term ‘relation application’ in literature. See also: relation composition. —James Haigh (talk) 2015-09-08T04:24:17Z

Function vs Function symbol

@Jochen Burghardt, you're right, I should have been clearer, but I do believe "function symbol" is right. It is not that X is the domain of f, but rather, X is the domain set we are about to assign to f.

And we really do mean "symbol", not the function itself. For example, { (0,0), (1,1), (2,2) } is a function, but we wouldn't use this in that axiom. – Farkle Griffen (talk) 22:52, 13 January 2025 (UTC)[reply]

It might be better to separate the function from the symbol.

Maybe "Given some relation R such that R is a function with a domain X and codomain Y, and a function symbol 'f' ..." – Farkle Griffen (talk) 22:57, 13 January 2025 (UTC)[reply]

I agree that one wouldn't write e.g. { (0,0), (1,1), (2,2) }(x) to denote a function application, so "symbol" seems indeed to be important.

On the other hand, the axiom schema (btw: which one exactly do you mean? Zermelo–Fraenkel_set_theory#Axiom_schema_of_replacement?) should apply to all functions, independently of whether they have got a name or not, so "symbol" there is inappropriate, imo.

In your above answer, I didn't understand why you introduced a relation symbol R (which was never used before in Function_application#Set_theory). What about Given any symbol f denoting a function with a given domain X and codomain Y, ...? - Jochen Burghardt (talk) 20:04, 14 January 2025 (UTC)[reply]

There's two notions of "function" that we're dealing with here: I'll call these "functions" and "set-functions". In first-order logic (which ZF is defined in), functions are primitive objects, so "function application" doesn't really need to be defined. But in the language of ZF set theory, there are no functions, and so "function application" doesn't exist, all we have are set-functions (sets of ordered pairs).

If we want to define bona-fide function application in ZF, we have to add a function letter to the language for the set-function we want to realize. The second source I added to that section (Mendelson) explains adding a function letter to a first-order language.

There are some ambiguity issues if we let the same letter denote the set and the function, and it seems like it would only be more confusing for the reader if we do it like that, which is why I suggest introducing R. – Farkle Griffen (talk) 19:59, 22 January 2025 (UTC)[reply]

"btw: which one exactly do you mean?"

This would be introducing a new axiom to ZF to define the new function letter (so, technically this would be a different theory, but it's a conservative extension, so it doesn't add anything apart from convenience). – Farkle Griffen (talk) 20:15, 22 January 2025 (UTC)[reply]