# How do we express higher arity predicates and functions in terms of membership?

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.

• The representation of relations and functions in set theory is standard and very well-known. What specific problems do you have with it? – Rob Arthan Jan 22 '15 at 21:54
• I only see the illustration of R(x) as x $\in$ R. Given R returns a truth value rather than the domain of discourse, I don't know how to turn R(f(x)) into anything similar, or how to turn R(x,y) into x $\in$ ? I want a procedure to convert higher order logic, (or second or first order logic) statements into first order statements using the membership predicate; without type construction and currying if possible. – dezakin Jan 23 '15 at 0:27
• Sorta reading lecture notes on Cartesian products representing sets for ordered pair relations, so I think I have an idea, but I'll have to play around with it. Think this might be the right track for relations, but not quite sure about functions yet. – dezakin Jan 23 '15 at 0:38
• Oh. Now it's sort of obvious, like most things after I understand them. I can study this over the next several days and write my own answer I guess. – dezakin Jan 23 '15 at 0:51