First orderer logic completeness and independence: the proof that disappear?

Question

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?

Answer 1

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.