Few days ago I asked about $WKL\_0$ and the role of binary trees to provide for completeness for first order theories, and the question was nicely answered by Joel David Hamkins: [Does $WKL\_0$ plus CON(PA+X) give a binary tree model of PA+X?](https://mathoverflow.net/questions/268391/does-wkl-0-plus-conpax-give-a-binary-tree-model-of-pax)


What kind of models are suggested from out of $RCA\_0$ to obtain weak completeness?



How does $RCA_0$ achieve weak completeness?
I also found the theorem confusing at first until I realized what is going on. 
Simpson is claiming that if you have a consistent theory $T$ that is closed under deduction, then in $RCA\_0$ you can prove that it has a model. 


What is confusing about the theorem is that one ordinarily thinks of the completeness theorem as involving, at its essence, a paths-through-trees argument, as I explained in [my answer to your earlier question](https://mathoverflow.net/a/268392/1946). 


Namely, if you have a consistent theory $T$, then you can add the Henkin assertions to it and still have a consistent theory, and then you build a tree of attempts to complete this theory: at each level, include the next sentence or its negation, provided that this is not yet revealed as inconsistent. Any path through this tree provides a complete consistent Henkin theory, which can be used to build a model. 


And conversely, one can show that the completeness theorem implies the weak Konig's lemma, since you can write down the theory of what it would be like to have a branch through a given tree, and this is a consistent theory, but any model would give you an actual branch. 


For this reason, we don't expect to get models of consistent theories without assuming something like $WKL\_0$. But $RCA\_0$ is exactly missing the weak König assertion, and so how is Simpson able to get the model in just $RCA\_0$? 


The answer is that the assumption that the theory $T$ is closed under deduction is stronger than one might think at first. For example, we cannot use this theorem to find a model of ZFC, even assuming Con(ZFC), or a nonstandard model of PA, because there is no computable extension of PA or ZFC that is deductively closed, since such a theory could be used to provide a computable separation of a computably inseparable pair, which is impossible. So in the standard model of $RCA\_0$, which has only the computable sets, we have ZFC and PA as computably-axiomatized theories, but there is no computable deductively closed theory containing them. 


Indeed, one can prove from $WKL\_0$ that every consistent theory $T$ is contained in a consistent deductively closed theory $T^+$, and indeed, a consistent complete theory $T^+$, since the tree of attempts to complete the theory is computable from $T$, and every branch through it provides a completion, as desired.


Meanwhile, if $T$ is deductively closed, then we can computably from $T$ build a complete consistent Henkin theory, using only $RCA\_0$. Namely, add the Henkin assertions, and then add each sentence or its negation if this is still consistent. The answer to the consistency question can be answered by consulting only the original theory, because you are asking if a certain sentence, combined with the sentences you have already added to the theory, implies a contradiction, and it if does, that implication assertion will itself be part of the original theory, since it is deducible from the theory. As Emil mentioned in the comments, this amounts exactly to the [computable completeness theorem](http://logic.uconn.edu/wp-content/uploads/sites/508/2014/01/effectivecompleteness.pdf). This is the assertion that for any decidable theory $T$, there is a decidable model of $T$. Or relativizing, every theory $T$ has a model computable from the deductive closure of $T$. 


So ultimately, there is no avoiding the paths-through-trees argument. But the point of the weak completeness theorem is that it suffices to just get the deductively closed theory first, and then afterwards find the complete consistent Henkin theory extending it, and this latter part no longer needs paths-through-trees once one has a deductively closed theory.


