Well, consider set theory extended with the ability to define functions
and then use them in terms. This is syntactically richer than the first
order language with one binary relation. The term language could allow for
various kinds of recursive definitions and have a nontrivial type structure.
I believe that there is a great variety of languages which are can be viewed as
syntactic sugar for set theory. I believe that the sugar is pragmatically
important. For example, in many such languages well-typedness can be checked
algorithmically. Terms provide the syntactic structure necessary for equational
reasoning based on the substitution of equals for equals and for term
rewriting. A translation into and out of pure set theory would lose the
struture used in both type checking and term rewriting. It seems that
a syntactically rich variant of set theory is desirable. But is not clear
taht any one such system will allow for all the heuristically useful
syntactic structure that people will invent in, say, future type systems.
David