I believe that it's true (correct me if I'm wrong) that
- When we predicate something of an argument we're saying that that argument is a member of a set intensionally defined just by that predicate? (I.e. '$Px$' := '$x\in P$ ')
- The $P$ in $Px$ is a monadic relation.
- The '$\in$' in '$x\in P$ ' is a dyadic relation.
It seems strange that the two expressions use different relations despite denoting the same thing. I suspect I'm wrong about one of the three points I listed above. Is there anything that I misbelieve?
In the "pure" language of predicate logic (or FOL) there is no symbol $\in$.
The usual "restricted quantifier" symbol : $(\forall x \in A) \ P(x)$ is an abbreviation for :
When we use it for the first-order language of set theory we need only one predicate symbol, the binary $\in$.
With it we can build atomic formulae, like : $x \in y$, and sentences, like : $\exists x \forall y \lnot (y \in x)$.
The (not trivial) difference is that in "pure" first-order language the expression $P(x)$ is formed with an individual variable symbol : $x$ and a unary (monadic) predicate symbol : $P$.
In the first-order language of set theory, the expression $x \in y$ is formed with two individual variable symbols : $x$ and $y$, and a binary (dyadic) predicate symbol : $\in$.
The "link" between $P(x)$ and $x \in P$ is thorugh the semantics; when we specify an interpretation $\mathcal I$ with domain $D$ for the language, we have to interpret the predicate symbol $P$ with a subset $P^D$ of the domain, i.e. $P^D \subseteq D$.
This interpretation assign a meaning to the atomic formula $P(x)$ throug a variable assignment function :
i.e. a function mapping individual variables to elements of the domain $D$.
The semantic specification for $P(x)$ will be :