Define an infinite tree as any set of sequences closed under prefix restriction, i.e. any prefix restriction of a sequence in the set is also in the set, where a prefix restriction is a restritcion of the original sequence to an initial segment of it (the prefix). In our case, we are interested mainly in countable trees, so we may take trees to be sequences of natural numbers closed under restriction. A computable tree is a tree such that there is an algorithm for computing, for each sequence, if it belongs to the tree. Finally, a branch through a tree is an infinite sequence such that each finite prefix of this sequence is in the tree. (I hope these definitions are correct; I'm still getting used to working with trees)
It is well-known that it is possible to construct an infinite computable tree such that none of its branches are computable, e.g., the Kleene tree. However, I remember reading somewhere that another way of constructing such a tree would be to use Peano Arithmetic; something to the effect that the tree would consist of formulas of PA, and if one could compute every branch, this would imply the decidability of PA. Unfortunately, I don't remember where I read this and I couldn't reconstruct the proof by myself. Does this strategy sound plausible? If so, could anyone help me to reconstruct this proof?
Yes, this is a standard example.
Fix a computable listing of the sentences in the language of arithmetic, $\{\varphi_i: i\in\mathbb{N}\}$. Each binary sequence $\sigma\in 2^{<\omega}$ now corresponds to a set of sentences: $$[\sigma]=\{\varphi_i: \sigma(i)=1\}\cup\{\neg\varphi_i: \sigma(i)=0\}.$$ (Note that this set is finite, since $\sigma$ has finite length.)
Now, say that $\sigma\in 2^{<\omega}$ appears consistent with $PA$ if there is no proof of $0=1$, of length at most $\vert\sigma\vert$, from $\sigma$ together with the first $\vert\sigma\vert$-many axioms of $PA$ (using some standard enumeration of $PA$, here). Since this is a purely finitary property, the question "Does $\sigma$ appear consistent with $PA$?" can be answered effectively: the set $$T=\{\sigma\in 2^{<\omega}:\sigma\mbox{ appears consistent with $PA$}\}$$ is computable.
This $T$ is our tree. It's easy to see that it is a tree - that is, $\sigma\in T$ and $\tau\prec\sigma$ implies $\tau\in T$. To see that it has no infinite paths, note that if $f$ is a path through $T$ then $\{[\sigma]: \sigma\prec f\}$ is a complete consistent extension of $PA$, which is computable from $f$. So we are done.
This is actually an example of a more general phenomenon. Say two disjoint r.e. sets $A, B\subseteq\omega$ are recursively inseparable if there is no computable $C$ with $A\subseteq C$ and $B\cap C=\emptyset$ (note that we could swap $A$ and $B$ and the definition would stay the same - replace $C$ by $\omega\setminus C$). Given any pair $A, B$ of recursively inseparable sets, we can form a tree $T_{A, B}$ of partial separations: $$T_{A, B}=\{\sigma\in 2^{<\omega}: \forall n<\vert\sigma\vert, [\sigma(n)=1\implies n\not\in B_{\vert\sigma\vert}]\wedge [\sigma(n)=0\implies n\not\in A_{\vert\sigma\vert}]\}$$ (where $D_s$ is the stage-$s$ approximation to $D$, if $D$ is an r.e. set (we assume a fixed recursive enumeration of $D$)). This $T_{A, B}$ is a recursive tree with no recursive path.
In the above example, we're using the recursively inseparable pair $\{$things $PA$ proves$\}$ and $\{$things $PA$ disproves$\}$.