1
$\begingroup$

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?

What kind of models are suggested from out of $RCA_0$ to obtain weak completeness?

$\endgroup$
14
  • 1
    $\begingroup$ @EmilJeřábek I am a little confused by the theorem. It would be kind of you to post an answer explaining how we should think about the difference between this "weak" completeness theorem and usual completeness theorem, which requires $WKL_0$. $\endgroup$ Apr 28, 2017 at 13:12
  • 1
    $\begingroup$ I guess the point is that you have to start with a theory that is already closed under consequence (which usually we don't have). For example, I can't get a computable model of ZFC using this theorem, since although ZFC has a computable axiomatization, the closure under consequence of it is not computable. And the point of the weak completeness theorem is that finding this closure-under-consequence is the hard part of finding the model of the theory, in the sense that you only need $RCA_0$ to do the rest of the work. Is that right? $\endgroup$ Apr 28, 2017 at 13:18
  • 2
    $\begingroup$ @Joel I don’t think I understand the theorem any better than you do. I guess the point is that if $T$ is a deductively closed theory, it behaves in $RCA_0$ as if it were decidable. That is, the standard inductive completion procedure produces a Henkin completion of $T$ which is computable relative to the deductive closure of $T$, and this argument can be formalized in $RCA_0$ if the deductive closure of $T$ is given as a set. $\endgroup$ Apr 28, 2017 at 13:42
  • 1
    $\begingroup$ @FrodeBjørdal No, that doesn't suffice, since there is no computable theory extending ZFC (or PA, or even Q) that is deductively closed, and so in the standard RCA_0 model, we would have Con(PA), but no class that was a deductively closed extension of PA. This is basically the argument that Simpson makes in his book on the pages following that theorem. $\endgroup$ Apr 28, 2017 at 17:15
  • 1
    $\begingroup$ I think Joel was replying to Frode’s last-but-one comment. Yes, $\exists Y\,\forall n\,(n\in Y\leftrightarrow\Pi_Tn))$ is exactly what is needed. $\endgroup$ Apr 28, 2017 at 17:57

1 Answer 1

3
$\begingroup$

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.

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. 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.

$\endgroup$
2
  • $\begingroup$ Many of these matters are confusing, and I have difficulties with accepting some statements of $WKL_0$ as I do not believe there is a non-paradoxical full binary tree. But perhaps others (Wikipedia?) state $WKL_0$ more cautiously in terms of finitely branching trees, and that this is more acceptable to me than the way Simpson states things. I see that there is (path-) choice involved with making a Henkin style sentential model for a given theory. But must we believe that there is a tree through which the choices are made? It seems that if the theory is decidable, it itself makes the choices. $\endgroup$ Apr 29, 2017 at 0:47
  • $\begingroup$ My previous comment does not attempt to contradict what you say, but express some of my prejudices and articulates parts of my attempts to understand some of the issues. Most likely we at fundamental levels agree. Some days of the week I believe that there are even $\Sigma_2$-admissible ordinals, but lately I am other days of the week in doubt as to whether there are even impredicative ordinals. $\endgroup$ Apr 29, 2017 at 0:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.