Does $WKL_0$ plus CON(PA+X) give a binary tree model of PA+X?

Question

In the context of reverse mathematics $WKL_0$ is considered equivalent to Gödel's completeness theorem over $RCA_0$. Does this mean that e.g. $WKL_0$ plus the consistency statement CON(PA+X) gives a binary tree which somehow is a model of PA+X?

Answer 1

The main idea is that the Henkin proof of the completeness theorem is esentially a paths-through-tree argument.

If $T$ is any consistent theory in a finite language, let $\tau$ be the tree of attempts to build a complete consistent Henkin theory extending $T$. So we add the Henkin assertions to $T$, and then at each level of the tree, we add the next sentence or its negation, if this is not yet seen to be inconsistent. So this is a finitely branching infinite tree, and any branch through this tree gives you a complete consistent Henkin theory, which gives you a model of the theory. So the essence of the completeness theorem is knowing that your tree has a branch.