In some sense, composition generalizes evaluation. The trick is, instead of writing $f(x)$ for $x$ an element of the domain of $X,$ we write $f \circ x$ for $x$ a function $1 \rightarrow X$. Similarly, inclusion generalizes membership (in some sense). The idea is that instead of writing $x \in X$ and calling $x$ an element, we write $x \subseteq X$ and demand that $x$ be a singleton.
Now these observations wouldn't be so interesting if composition/inclusion were ill-behaved relative to evaluation/membership. If anything, though, the opposite is true. In particular:
- composition is associative, evaluation is not.
- inclusion is transitive, membership is not.
Of course, the evaluation/membership duo is partially redeemed by its good extensionality properties. In particular:
- If $f$ and $g$ have domain $X$, then if for all $x \in X$ we have $f(x)=g(x)$ , then $f=g$.
- If $A,B \subseteq X,$ then if for all $x \in X$ we have $x \in A \leftrightarrow x \in B$, then $A=B$.
However, we can rehash the above observations (or axioms or whatever) into statements involving only composition/inclusion.
- If $f$ and $g$ have domain $X$, then if for all $x : 1 \rightarrow X$ we have $f \circ x=g \circ x$ , then $f=g$.
- If $A,B \subseteq X$, then if for all singletons $x \subseteq X$ we have $x \subseteq A \leftrightarrow x \subseteq B$, then $A=B$.
So, I'm wondering: can we found mathematics without using the notions of evaluation/membership?
I know for example that categorial set theories like ETCS make a big leap in this direction. However, as far as I know, all such theories are still based on classical first-order logic. Thus, we have expressions like $g \circ f$, which basically denote the function $\circ$ being evaluated at $(g,f).$ So, we haven't completely banished evaluation, just lessensed its prominence.
Furthermore, first-order logic also features expressions like $\forall x Px.$ However, this is conceptually equivalent to an expression like $\forall(P).$ Basically, we're thinking of $\forall$ is a function $\mathrm{Predicates} \rightarrow \mathbb{B}$, that accepts a predicate $P$, and returns a truthvalue $\forall(P),$ which is true iff $P$ returns true on all possible inputs. So in some sense, the expression $\forall x Px,$ being essentially the same as $\forall(P),$ still involves evaluation. I'd rather have something more like $\forall \circ P,$ whatever that means.
In summary, I'm curious to know: is it possible to found mathematics in a way that makes absolutely no use of evaluation or membership, even at the level of the logic?
Ok, so basically I now think I get what you wanted.
Actually you can use ETCS as foundational theory (to be exact to have a theory that is completely equivalent to ZFC, which most people consider the basic foundational theory, you need to ad another axiom which plays the role of replacement axiom).
The idea to codify all the object of a (multisorted)-first order language in the following way:
sorts of the theory are interpreted as object (i.e. sets) in the category;
every constant symbol $c$ of type $X$ is interpreted as a morphisms (i.e. a function) of type $c \colon \bullet \to X$ (here $\bullet$ denote the singleton);
every function symbol $f$ of type $A \to B$ is just a morphism $f \in \mathbf{Set}(A,B)$;
a relation $R$ of type $A_1,\dots,A_n$ is interpreted as subobjects i.e. monomorphisms $r \colon R \hookrightarrow A_1 \times \dots \times A_n$.
Then all the logical operation can be codified as operation on such object via limits and colimits which are provided in the category of sets.
In such framework a term of type $f(c)$, where $f$ is a function symbol of type $A \to B$ and $c$ is a constant of type $X$, is the morphism $f \circ x \colon \bullet \to Y$, which is again a constant.
Membership can be codified too in a different sort of way.
The idea is that every set must be a subset of some sort, meaning that we want to identify sets with the unary predicates defining them. Using this fact we can interpret sets of elements of type $X$ as monomorphism of type
$$p \colon P \hookrightarrow X$$
with this in mind a constant $c \colon \bullet to X$ belong to $P$ iff there's a morphism in $\mathbf{Set}$, let's call it $\tilde x \colon \bullet \to P$ such that $x = p \circ \tilde x$. In this way we can defined $x \in P$ as an abbreviation for $\exists \tilde x \colon \bullet \to P \ x = p \circ \tilde x$.
The interesting fact about all this construction is that it can be done not just in the category of sets,(i.e. in the theory ETCS) but also in the theory of every other category with enough structure, for instance in every topos.
I think you could find interesting the following links
about ETCS you may find interesting this article of Leinster.
Edit: An additional information, when dealing with the axiomatic theory ETCS you can avoid the use of the function symbol $\circ$ and use instead a ternary relation $\circ(x,y,z)$ which should be interpreted as $z$ is the composite of $x$ and $y$ (i.e. as $y \circ x = z$). Then you have to rephrase all the other axioms for category with this ternary relation (the axioms of associativity, identity, those that tell when the composition has sense). In such theory you cannot build terms via composition, so you don't have any application of functions. Of course you can reintroduce application/composition as symbolic abbreviation for the formulas build from the $\circ(x,y,z)$ with the connectives.