undecidable statement of the form "$F$ is a choice function on $M$"

Question

Are there unary predicates $\varphi(x), \psi(x)$ such that

1. The formula that states "There is a set $M$ with: $\forall x[x\in M \leftrightarrow \varphi(x)]$" is provable in $ZFC$.

2. The formula that states "There is a set $F$ with: $\forall x[x\in F \leftrightarrow \psi(x)]$" is provable in $ZFC$.

but the formula that states "$F$ is a choice function on $M$" is not decidable in $ZFC$?

Answer 1

Sure. Let $G$ be some undecidable sentence of ZFC, and let $$ \begin{align} \varphi(x) &\equiv x=\{42\} \\ \psi(x) &\equiv G \land x=\langle\{42\},42\rangle \end{align} $$

Answer 2

Surely this is over simplistic, but this is an "obvious" example.

Take $\varphi(x)$ to be the predicate "$x$ is a non-empty set of finite ordinals", then $\sf ZF$ proves that there is some $M$ such that $\forall x(x\in M\leftrightarrow\varphi(x)$.

Take $\psi(x)$ to be the predicate "If $V=L$ holds, then $x=\langle y,n\rangle$ such that $\varphi(y)$ and $n=\min y$; If $V\neq L$ holds, then $x\neq x$". Then in models of $\sf ZFC$ satisfying $V=L$, $F$ defines a choice function from sets of finite ordinals, and in models satisfying $V\neq L$ it is the empty set which is certainly not a choice function on $M$.