This is a followup to this question. I am trying to formalize an intuitive notion/question: Is it always possible to write down necessary and sufficient conditions (i.e. formulas) for a property $P$?
Let $\mathcal {Y,X}$ be two arbitrary sets, and $f:\mathcal X\to\mathcal Y$ some function.
Let $\mathcal L_{\mathcal X}$ be a language in first order logic over some set $\mathcal X$, i.e. containing propositional formulae and quantifiers only over $\mathcal X$. A set $X\subseteq\mathcal {X}$ is called "characterizable in $\mathcal L_{\mathcal X}$" if we can write down an $\mathcal L_{\mathcal X}$-formula $\phi_X(x)$ such that $\phi_X(x)$ is true iff $x\in X$. Similarly for $Y\subseteq \mathcal{Y}$ if there is such a formula $\phi_Y(y)$ in a language $\mathcal L_{\mathcal Y}$.
A function $f$ is called "characterizable" if we can write down an $\mathcal L_{\mathcal X, \mathcal Y}$-formula $\phi_f(x,y)$ such that $\phi_f(x,y)$ is true iff $f(x)=y$.
Conjecture. If a set $Y\subseteq \mathcal Y$ is characterizable in some $\mathcal L_{\mathcal Y}$, and $f:\mathcal X\to\mathcal Y$ is characterizable in some $\mathcal L_{\mathcal X, \mathcal Y}$, then $X=f^{-1}(Y)$ is characterizable in some language $\mathcal L_{\mathcal X}$.
Does this formalism capture the desired intuition well? (that we can always write down "necessary and sufficient conditions").
Does this definition of "characterizable" already exist?
Is this conjecture correct?