We can create a function (let me call it $¬$) that maps a function and it's input to the value of $f$ at $x$, look at this previous Previous question of mine I discuss the idea of this, my question is entirely based on the kind of notation that we use here, and moved to a separate question to give others a chance to answer it. Let $¬$ denote the function that maps $(f,x)$ to $f(x)$ we can use $¬$ as a binary operator such that $f(x)=f¬x$.
My question is if the notation $f(x)$ is actually a shorthand for $f¬x$? In the same way $a\times b$ can be written for ease as $ab$ in algebraic expressions, the implication of this would be that $f(x)$ implies that we need to use the function $¬$ to 'apply' $f$ to '$x$', and hence $¬(f,x)$ would be actually the value of $¬$ on $¬$.
This leads to issues however, if the value of our 'application' function is given a special name '$f(x)'$ then what denotes the value of $f$ at $x$, do 'application' functions have a special property that we can denote it's value but we cannot do this for $f$ at $x$?
Is it that 'application' can be described as a function but a function is not required to do so, it is simply associating a number with the function at a given input?
In the standard set-theoretic framework for formalizing math, functions are sets (binary relations satisfying certain properties, as discussed on your previous question) and are therefore "first-class objects" that live inside the domain of discourse and obey the rules of set theory. This allows us to formally prove abstract statements about functions, like "the composition of two surjective functions is surjective", as theorems about sets.
The operation of function evaluation (not restricted to functions $X\to Y$ for some fixed $X,Y$) is not a function in this sense. It is a class function, which means we have a syntactic formula $\phi(f,x,y)$ about sets (in this case "$(x,y)\in f$") such that whenever $f$ is a function and $x$ is in the domain of $f$, there is a unique $y$ satisfying $\phi(f,x,y)$; this justifies introducing the notation $f(x)$ to refer to that $y$. This is called extension by definitions, and it effectively adds a symbol (which you've called $\lnot$) to the language of set theory alongside $\in$. Symbols at this level are not part of the universe that they operate on, so expressions like $\lnot(\lnot,f,x)$ are malformed, and theorems we prove about set functions don't directly apply to class functions. Studying these language-level objects requires more tools from metamathematics.