Notation: $P(x)$ iff $x$ has property $P$

Question

In set theory (for example), people write $P(x)$ to indicate that $x$ has property $P$. What is the meaning of this "expression" formally? Is $P$ a predicate (a Boolean-valued function on some set [what set?]) that returns $\top$ iff $x$ has property $P$? If this is the case, then shouldn't one write $P(x)=\top$ instead of $P(x)$?

Answer 1

No, if $P(x)$ is some formula of set theory (like $\exists y \forall z\colon z \in x \rightarrow z \in y$), then it's not a function. Also, $\top$ isn't in alphabet of set theory, and only terms (expressions value of which is set) can appear at left (or right) of symbol $=$.

If you use set theory to build a model of another theory (even of set theory itself) - it becomes another story. Then formula of this modeled theory can be considered as denoting some subset of model. For example, if we want to model Peano arithmetic, we can take some set as support of model (for example, set $\omega$), and define $+_{PA}$ and $\cdot_{PA}$ as functions on it, and $\leqslant_{PA}$ and $=_{PA}$ as subsets of $\omega \times \omega$. But "for PA" it will not be sets or functions - it will be just symbols.