Gödel completeness theorem for the first-order logic is in fact equivalent to BPI (every proper filter can be extended to an ultrafilter). Moreover, BPI is independent of ZF; that in particular means that ZF+$\neg$BPI proves that there exist a set of sentences $T$ and a particular sentence $\sigma$ such that $\ulcorner T\urcorner\models\ulcorner\sigma\urcorner$ but there's no proof of the latter from $\ulcorner T\urcorner$. If $T$ has a computable list of axioms, the "$Prf_T$" predicate is also computable, and so we could decode $T$ and $\sigma$ and check if effectively $T\not\vdash\sigma$. But the same argument can be performed for ZF+BPI which, instead, believe that for every theory and for every sentence, if the latter is a logical consequence of the former, then there exists a proof, and so, the same holds for $T$ and $\sigma$.

Therefore the question is: in order to avoid contradictions about the existance of the proof of $\sigma$ from $T$, must we conclude that the code number of the proof of $\ulcorner\sigma\urcorner$ from $\ulcorner T\urcorner$ in ZF+BPI is non-standard? Or must we deduce that the theory $\ulcorner T\urcorner$ that attest $\models\,\not\Rightarrow\,\vdash$ in ZF+$\neg$BPI cannot be effectively axiomatized? Or what else?


The complexity of $T$ is indeed the issue, but on a much grander scale than you're considering. When you ask whether $T$ is "computationally simple" (e.g. effectively axiomatizable) you're automatically assuming that the language of $T$ is countable (and indeed that you've fixed a method of numbering the sentences in the language of $T$). But this isn't the case for an arbitrary first-order theory.

ZF proves the following version of the completeness theorem:

Suppose $T$ is a theory in a well-orderable language and every model of $T$ satisfies $\varphi$. Then $T\vdash\varphi$.

This is because, relative to a well-ordering of the set of all relevant sentences, we can run Henkin's completeness argument perfectly explicitly. Where choice - or rather, a fragment of choice - kicks in is when we try to handle non-well-orderable languages (or, if we have full choice, when we argue that all languages are well-orderable).

In particular, any countable set is well-orderable, so ZF alone proves completeness for all countable theories. So ZF proves the completeness theorem for basically every theory that actually is relevant to mathematical practice. (The one exception I can think of is the language of nonstandard analysis, where in order to get full transfer we want symbols for every function on the reals.)

You ask also about "missing proofs." Actually it's the other way around: you should be worried about missing models.

Specifically, suppose I have a consistent (= $\not\vdash\perp$) theory $T$. Henkin tells me that, from a well-ordering of the language of $T$, I can build a "really complete" theory containing $T$, whose term model('s reduct) is then a model of $T$. If I'm working in a model of ZF alone, however, I might not have such a well-ordering, and so I won't be able to build a model of $T$.

That is, when we see in ZF a failure of completeness, it's not because we don't have enough proofs, it's because we don't have enough models. One way to see this "concretely" is via forcing (which admittedly is far too complicated to describe here, but the point is it's a method for building models of ZF(C) "to order"): starting with a model $M$ of ZF and a theory $T$ in $M$, we can force over $M$ to make $T$ well-orderable (e.g. force with $Col(\omega,T)$). In the resulting forcing extension $N$, the theory $T$ is now well-orderable and so Henkin's argument shows that $N$ contains a model of $T$. But forcing doesn't add any new finite sequences of things we already have - such as sentences in the language of our theory - so we haven't "gained proofs" in any sense; rather, our space of models has increased.

  • $\begingroup$ (+1) To make more contact with the OP's framing, the semantic consequence is $T\models \bot$ whereas if $T$ is consistent, $T\nvdash \bot,$ so it's not the lack of proof witnessing inconsistency but the lack of a model witnessing $T\not\models \bot.$ $\endgroup$ – spaceisdarkgreen Feb 16 '19 at 1:32
  • $\begingroup$ (And here I think $T$ could be something like the theory of $B$ in the language of Boolean algebras plus constants from $B$, augmented with a symbol $U$ and the statement that $U$ is an ultrafilter on the domain. (Where $B$ is a Boolean algebra with no ultrafilter on it.)) $\endgroup$ – spaceisdarkgreen Feb 16 '19 at 1:35
  • $\begingroup$ I agree with all of this except for the very end, "forcing ... doesn't add any new natural numbers, so we haven't gained proofs." This seems to assume proofs amount to numbers, which they won't in a non-well-orderable language. I think what you want is that forcing won't add new finite sequences of elements from ground-model sets, and so won't add proofs in ground-model languages. $\endgroup$ – Andreas Blass Feb 16 '19 at 2:38
  • $\begingroup$ @AndreasBlass I would still say that a proof amounts to a natural number, after fixing a finite bit of information (namely, a numbering of an appropriate finite subset of the language) in an appropriately-benign way. But I agree that in this context it could be clearer. Fixed! $\endgroup$ – Noah Schweber Feb 16 '19 at 2:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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