Can every functional equation be solved or proved unsolvable?

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:

1. $$f : \mathbb{R} \to \mathbb{R}$$ is a real-valued $$1$$-ary function.

2. $$+ : \mathbb{R} \times \mathbb{R} \to \mathbb{R}$$ is the usual addition.

3. $$- : \mathbb{R} \times \mathbb{R} \to \mathbb{R}$$ is the usual subtraction.

4. $$\cdot : \mathbb{R} \times \mathbb{R} \to \mathbb{R}$$ is the usual multiplication.

5. $$\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}$$.

• Your statement of Wilkie's resolution to the high school algebra problem is imprecise. It doesn't make any sense to say that the identity "cannot be proved under $(\mathbb{N},+,\times,\mathrm{exp})$": structures don't prove theorems, axioms do! The correct statement is that Wilkie's identity is true in the structure $(\mathbb{N},+,\times,\mathrm{exp})$, but not provable from the particular set of 11 "high school axioms" that Tarski specified. Dec 1, 2021 at 16:01
• Oh, and I just noticed that near the end of your question you claim that Tarski's high school algebra problem is independent of $\mathsf{ZFC}$. Hardly! In fact, it's easy to prove (using much less than $\mathsf{ZFC}$, e.g. $\mathsf{PA}$ and weaker systems can do it) that Wilkie's identity holds in $\mathbb{N}$. Again, the fact is just that Wilkie's identity is independent from the very weak system of 11 axioms specified by Tarski. And Wilkie's resolution of the high school algebra problem is of course a proof in $\mathsf{ZFC}$. Dec 1, 2021 at 16:04
• Note that the a priori upper bound on the complexity of solvable functional equations is quite high, namely $\Sigma^{\color{red}{2}}_1$ (it drops down to $\Sigma^{\color{green}{1}}_2$ if we restrict attention to, say, continuous solutions - moreover, if we do that Shoenfield absoluteness kicks in and shows that (un)solvability of a given functional equation can't be changed by forcing for example). Dec 1, 2021 at 20:26
• I don't know about this problem, but some of its variants would be undecidable. For instance if we allow constants and the $\sin$ function, we can reduce solvability of polynomial equations over $\mathbb Z$ to this problem: take a polynomial $P(x_1,\dots,x_n)$ over $\mathbb Z$, and consider $F(f)=P(f(1),\dots,f(n))^2+\sin(\frac1\pi f(1))^2+\dots+\sin(\frac1\pi f(n))^2$ and $G(f)=0$. You can probably get around having to use the constant there. However getting this to work with just $\exp$ sounds much harder - it's believed that $\mathbb Z$ is not a definable in $\mathbb R$ with exponentiation. Dec 11, 2021 at 11:25
• See also Richardson's theorem - doesn't answer the question, but is similar in spirit. Dec 11, 2021 at 11:44