Recently, I have read articles about how some identities whose "solution" either cannot be determined within $\mathsf{ZFC}$ or other axiomatic systems or the solvability is closely related to the consistency of the axioms. Here are a few examples:
Tarski's high school algebra problem. In 1980, Alex Wilkie proved that the identity: $$ \left((1+x)^y+(1+x+x^2)^y\right)^x\cdot\left((1+x^3)^x+(1+x^2+x^4)^x\right)^y\\=\left((1+x)^x+(1+x+x^2)^x\right)^y\cdot\left((1+x^3)^y+(1+x^2+x^4)^y\right)^x $$ cannot be proved by the "high school axioms" listed by Tarski.
In this MathOverflow post, it says that a polynomial $P(x_1,\dots,x_n)$ has been explicitly computed such that it is solvable in the integers iff $\neg\operatorname{Con}(\mathsf{ZFC})$.
Now I am personally a fan of functional equations and I enjoy toying with them in my free time. Thus, I am curious if there are similar things like the above but for functional equations. To do this, I shall make my question formal.
Consider the language $\{f,+,-,\cdot,\exp,\circ\}$, and interpreting each symbol as:
$f : \mathbb{R} \to \mathbb{R}$ is a real-valued $1$-ary function.
$+ : \mathbb{R} \times \mathbb{R} \to \mathbb{R}$ is the usual addition.
$- : \mathbb{R} \times \mathbb{R} \to \mathbb{R}$ is the usual subtraction.
$\cdot : \mathbb{R} \times \mathbb{R} \to \mathbb{R}$ is the usual multiplication.
$\exp : \mathbb{R} \times \mathbb{R} \to \mathbb{R}$ is the usual exponentiation ($\exp(x,y) = x^y$).
Note that I omitted division to avoid the annoyance of division by $0$.
A functional equation shall be defined as an equation $F(f,x,y,z,\dots) = G(f,x,y,z,\dots)$, such that $F$ and $G$ are legal compositions of the five functions defined above. We say that a functional equation is solvable if: $$ \mathsf{ZFC} \vdash \exists f\forall x \forall y \forall z\cdots[f : \mathbb{R} \to \mathbb{R} \wedge F(f,x,y,z,\dots) = G(f,x,y,z,\dots)] $$
Informally, we call attempting to solve for an $f$ in a functional equation a functional problem.
My question is that:
Is it possible to formulate an explicit functional problem which solvability is either independent of $\mathsf{ZFC}$ (like Tarski's high school algebra problem, but instead it's the "high school axioms" listed by Tarski), or is closely related to the consistency of $\mathsf{ZFC}$ (like the linked MathOverflow post)?
I'm also open to functional problems which is closely related to other relevant/interesting axiomatic systems instead of $\mathsf{ZFC}$.
