Let $G(x)(k)$ denote the $k$-th term in the Goodstein sequence starting at $x$, and $\gamma(x)$ denote the [least] $k$ such that $G(x)(k) = 0$. We know that neither $\gamma$ nor $TREES$ are provably total in $PA$.
Consider the sentence $\sigma = \exists x_{0} \forall x > x_{0} (TREES(x) > \gamma (x))$. Does $PA$ prove $\sigma$?
Further comments: consider a machine $M$ that computes $TREES$ and a machine $N$ that computes $\gamma$. Then $\sigma$ can be seen as asserting "for all sufficiently large $x$, on input $x$, $N$ halts before $M$". I can see for instance a model that thinks $\gamma$ is nontotal while $TREES$ is total thinking this sentence is false - at some nonstandard $x$, $\gamma$ will be undefined and thus $M$ will halt before $N$. The existence of such a model would imply the independence of $\sigma$ from $PA$. But can such a model exist?