Is it possible that Gödel's completeness theorem could fail constructively? Gödel's completeness theorem says that for any first order theory $F$, the statements derivable from $F$ are precisely those that hold in all models of $F$. Thus, it is not possible to have a theorem that is "true" (in the sense that it holds in the intersection of all models of $F$) but unprovable in $F$.
However, Gödel's completeness theorem is not constructive. Wikipedia claims that (at least in the context of reverse mathematics) it is equivalent to the weak König's lemma, which in a constructive context is not valid, as it can be interpreted to give an effective procedure for the halting problem.
My question is, is it still possible for there to be "unprovable truths" in the sense that I describe above in a first order axiomatic system, given that Gödel's completeness theorem is non-constructive, and hence, given a property that holds in the intersection of all models of $F$, we may not actually be able to effectively prove that proposition in $F$?

Given a sentence $\phi$ that holds in all models of a first-order theory $F$, you can effectively find a proof of $\phi$: just enumerate all proofs in $F$ until you find the one that proves $\phi$ (there is such a proof, since you are given that $\phi$ holds in all models of $F$ and hence, by the completeness theorem, you are given that $\phi$ is provable). So there are no unprovable truths in first-order logic.
The non-constructive nature of the proof of the completeness theorem is that it uses non-constructive methods to prove the existence of a model of a sentence that cannot be disproved. When you apply the theorem to some sentence $\phi$ that you can prove (maybe non-constructively) to be true in all models, finding the proof of $\phi$ is effective.
