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?



Does $WKL_0$ plus CON(PA+X) give a binary tree model of PA+X?
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. 


