It's been noted by others that higher order logic is similar to set theory. We can express the second order statement $\forall$R$\forall$x(R(x)) as a first order statement $\forall$R$\forall$x (x $\in$ R). This seems like a neat way of translating set theory into higher order logic, as well as proving logically valid statements about set theory in general semantics.
How can we translate higher arity functions and predicates into first order membership predicates?
$\forall$R$\forall$x$\forall$y(R(x,y)) or $\forall$R$\forall$f$\forall$x$\forall$y(R(f(x,y), x, y) for example.
I can imagine doing type construction to turn higher arity predicates and functions into monadic higher order predicates and functions though currying, but this seems a bit awkward, and the process of doing that isn't immediately obvious to me.