Let $f(0)=1$ and $f(x+1)=2^{f(x)}$
Also let f be infinitely differentiable. Then does f exist and is it unique?
If f is merely continuous, then any continuous function such that f(0)=1 f(1)=2 satisfies the conditions(if f is defined in [0,1] ,we can use the property to define it everywhere else). Similar things can be said for differentiability. But I don't how to solve the problem if it's infinitely differentiable.
On
Your question is an example of the question "can tetration be extended?" My approach uses fixed points to extend tetration, but there are an infinite number of solutions to $2^z=z$ in the complex plane, while no solutions exist in the real numbers. Since the real numbers don't contain a fixed point, neither can it contain $^\infty 2$ or $^{-\infty} 2$. On the other hand in the complex plane there are an infinite number of solutions for $^{-\infty} 2$, so $f(x)$ can't be unique.
A couple of years ago, Henryk Trappman and Dimitrii Kouznetsov published a proof of uniqueness for Hellmuth Kneser's tetration solution, which was published in 1950. Henryk and Dimitrii's paper from 2009 is here: http://eretrandre.org/rb/files/Trappmann2009_82.pdf
The uniqueness criteria for $\text{Tet}_2(z)=\exp_2^{[oz]}(1)$ boils down to
As $\Im(z)$ increases, $\text{Tet}_2(z)$ converges to the primary fixed point $z_0\approx0.8247+1.5674i$, such that $2^{z_0}=z_0$. Kneser's solution starts with the Schroeder function, $s(z)$, for 2^z, $\lambda=z_0\log(2)=\log(z_0)$.
$s^{-1}(\lambda z)=\exp_2(s^{-1}(z))\;\;\;\;s^{-1}(z) = z_0 + z + a_2 z^2 + a_3 z^3 + ...$
Then the inverse abel function for $2^z$ is $\alpha^{-1}(z)=s^{-1}(\lambda^z)$ where by definition $\alpha^{-1}(z+1)=2^{\alpha^{-1}(z)}$, which is close to what we're looking for.
But $\alpha^{-1}(0)$ has a singularity, and $\alpha^{-1}(z)$ is not real valued. Nontheless, as $\Im(z)$ increases towards imaginary infinity, $\alpha(\text{Tet}_2(z))\approx z+k$, where k is a limiting constant. As $\Im(z)$ increases, $\text{Tet}_2(z)$ and $\alpha^{-1}(z)$ both converge towards $z_0$. $\alpha(\text{Tet}_2(z))=z+\theta(z)$. theta(z) is a 1-cyclic function, $\theta(z)=k+\sum_{n=1}^{\infty}a_n\exp(2n\pi iz)$, which decays to the constant k as $\Im(z)$ increases.
$\text{Tet}_2(z)=\alpha^{-1}(z+\theta(z))$, theta(z) has singularities at integers, but is analytic for $\Im(z)>0$.
Then Kneser's tetration solution is generated by wrapping $z+\theta(z)$ around a unit circle via a Riemann mapping at the real axis for a unit interval. $y=\exp(2\pi i z)$. $\text{Riem}(y)=\exp(2\pi i\times(z+\theta(z))$. This is identical to Kneser's Riemann mapping for the unbounded region defined by $\exp(2\pi i \alpha(z))$ for z in the range 0..1. I hope this helps a little.
The $z+\theta(z)$ notation is ad-hoc notation for what I came up with to implement Kneser's algorithm in pari-gp. The code is posted here, http://math.eretrandre.org/tetrationforum/showthread.php?tid=486 It turns on the Riemann mapping has a very nasty singularity, and is very difficult to use to generate numerical results for tetration. The pari-gp algorithm has not been proven to to converge, but it seems to work very well. This code can calculate the Taylor series anywhere in the complex plane for tetration for arbitrary real bases>e^1/e.