Why do we use both sets and predicates? For every set S we can define s as $$ \forall x:s(x) \iff x \in S$$, and for every predicate p we can define $$P:=\{x|p(x)\}$$. Operations and their properties correspond, etc.
In every theorem or proof or definition, I believe, in principle, I could translate from set to predicate notation or vice versa. Would that change the meaning?
It seems to me that the only differences are superficial ones:
- syntax: xeP vs p(x)

- intuition: "bag" vs "question"

I assume logic and predicates are more basic and necessary. Hence, why use sets besides predicates if they are essentially equivalent?
Is the reason for using sets only for the sake of better intuition? Or because 1st order logic does not allow predicates on predicates, but sets allow us to circumvent that restriction? Or is it historical?
Please consider in your answer that I only have highschool level math skills, in case that was not obvious from my question :)
 A: The nifty thing about sets is that they are things. We can talk about functions whose values are sets, or functions that take sets as inputs, or make sets of sets, or sets of sets of sets ...
This is quite useful, and in fact absolutely ubiquitous in higher mathematics.
The downside of this is that when sets are "things", there can't be a set for any property of "things" that we can define. That's what Russell's paradox shows: if $\{x\mid x\notin x\}$ were a thing, then it would neither be nor not be an element of itself, which is absurd -- so it can't be a thing.
Of course that doesn't mean that we should refrain from ever speaking of a property that we have defined willy-nilly by stating what the condition for it is. We just need to be remember that such a propert is not a thing: it cannot necessarily be the value of a function, an element of a set, and so forth.
It is now convenient to have two different words for the two different rulesets we might be working under for the concepts we name.
The ones where we work by "is a thing but cannot be defined just by fiat" we call sets -- and then we need some explicit formal rules for how we can define a set, which are the axioms of set theory.
The ones where we work for "can be defined every which way but is not a thing", we call predicates. For historical reasons we often notate named predicates with a slightly different syntax than sets, but within set theory it is also common to use the same $\in$ notation as for sets, in which case we call them classes rather than predicates -- but it's the same concept in either case. In either case we need few axioms for them, because it's understood that a named predicate/class is formally just an abbreviation for the particular formula that defines it.
This works pretty well in practice.
Higher-order logic offers a different way out, where the same concept can at once be a "thing" at one level of the type hierarchy while being defined by free-wheeling fiat over lower levels of the hierarchy. At first glance this can look like it gives us the best of both worlds in one package. But in practice it turns out to be cumbersome to use for actual mathematics -- for example, if you take a quotient of a group, the elements of the quotient group are naturally sets of elements of the original group, so the quotient group exists on a different level of the type hierarchy. The fact that there's no level in the hierarchy that contains all groups we'll ever be interested in makes it difficult to formalize theorems about the relation between groups.
There are recent developments in type theory (where "recent" means the last 50 years or so) that aim at making this less cumbersome by allowing the system to internalize the meta-theorems one would otherwise need to state results that work on more than one type level. So far the results of this have not won general acceptance as a foundation for all of mathematics, though it's pretty widely used in the areas of automated theorem proving and machine-verified proof, for exampe with the HOL theorem prover.
A possible reason for this is that the formal rules of a useful non-cumbersome higher-order logic system are a lot more complex to state and explain than those of first-order logic and set theory. This puts the higher-order approach at a considerable didactic disadvantage -- but it may change in the future if machine-verified proofs really take off.
