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$?
 A: 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.
A: I should clarify that I believe all the math here is well-known folklore, but I haven't ever actually seen it written up or even stated explicitly. So this is not new, but it is original in the sense that I can't point you towards a reference.

There is a very interesting reverse mathematics question here. I'm not sure this is really what you're asking since you only bring up reverse math in passing and seem more interested in constructivism (note that reverse math uses classical logic), so perhaps this should be a comment as opposed to an answer. But $(i)$ I think you'll still find it interesting, and $(ii)$ it's just a bit too long for a comment.
The "naive" form of this question - we'll see below that there are some important subtleties which crop up when we try to express it precisely - is:
How complicated can validity be, consistently with RCA$_0$?
(Here by "valid" I mean "true in every structure" - and for $\Gamma$ a set of sentences, "$\Gamma$-valid" will mean "true in every model of $\Gamma$.")
I don't know the full answer, and in fact the question itself is much more complicated than it may first appear, but let me say some things.

Convention. Since we're talking both about models of RCA$_0$ (which we're thinking of as the contexts we're living in) and models of theories as understood by models of RCA$_0$, I'll use the term "universe" to describe the former. E.g. "there is a universe in which not every theory can be extended to a complete theory."


Unfortunately, before I begin there are some important subtleties to discuss. This gets a bit lengthy, but there's simply no way to honestly talk about the question at hand without addressing these points. If you'd like, you can skip this section and come back to it later, but it is important.


*

*FIRST, a convention about the contexts we'll consider here. Remember that RCA$_0$ is a theory in the language of second-order arithmetic: models of the theory consist of a "numbers" part - which satisfies a fragment of the usual axioms of Peano arithmetic - and a "sets" part, which satisfies extensionality (= two sets are the same iff they have the same elements) and some weak set formation axioms (roughly, "computable sets exist"). An $\omega$-model is a model of RCA$_0$ where the numbers-part is isomorphic to the usual natural numbers. Not every model of RCA$_0$ is an $\omega$-model, but the $\omega$-models form an important special class of models and are generally much easier to think about.


*

*Why is this important? Well, remember that models with nonstandard natural numbers will have nonstandard first-order formulas and sentences. And while satisfaction for standard formulas is well-behaved, when we pass to the nonstandard case things can get quite ugly (e.g. see here). So by focusing on $\omega$-models only, we get rid of some nasty pathologies - they're potentially interesting pathologies, but at least in developing the very basic picture we should avoid them at first.


*SECOND, and much more subtle, we need to get some precise definitions vis-a-vis satisfaction and validity. How do we define "$\models$" in the language of second-order arithmetic? (Note that the provability relation "$\vdash$" doesn't give us any problems.)


*

*Well, for each $n$ there is a natural formula $\psi_n$ defining satisfaction for theories consisting of sentences with at most $n$ quantifiers. These definitions work really well: for every universe $M$, every language $\Sigma\in M$, every structure $A\in M$, and every $\Sigma$-theory $T$ consisting of sentences with at most $n$ quantifiers, we have $A\models\theta$ externally iff $M\models\psi_n(A, T)$ (where I'm conflating ignoring coding/Godel numbering issues for now). This lets us define for each $n$ the "$n$th-level" of semantic entailment: for $T$ a theory consisting of sentences with at most $n$ quantifiers, we define $T\models_n(\varphi)$ to be the statement $$\mbox{ Every sentence in $T\cup\{\varphi\}$ has at most $n$ quantifiers and }\forall A(\psi_n(A, T)\implies \psi_n(A, \varphi))\}.$$ However, note that the $\psi_n$s don't yield a definition of satisfaction which applies to all sentences simultaneously - they force us to go "level-by-level." 

*That's ugly. Surely there's got to be a way to talk about general satisfaction in the language of second-order arithmetic! Well, there is, but it stinks a bit. Via the idea of Skolem functions, we can cook up a single $\Sigma^1_1$ formula $\xi$ which classically defines satisfaction of all first-order formulas in all structures simultaneously. However, this leads to a surprising problem: from the recursive perspective, Skolem functions don't always exist! For example, let $REC$ be the universe consisting of just the recursive sets, let $A$ be the structure $(\mathbb{N}; +,\times)$, and let $\theta$ be the sentence "For every $n$ there is some $k$ such that for all $m<n$, if the $m$th Turing machine halts on input $0$ then it halts in at most $k$ many steps." $\theta$ is definitely true in $A$, and indeed $M\models \psi_k(\theta, A)$ where $k$ is the number of quantifiers occurring in $\theta$, but any Skolem function for $A\models\theta$ corresponds to a function that grows at least as fast as the Busy Beaver function, and so no recursive Skolem function exists. Indeed, "Skolem functions always exist" is equivalent over RCA$_0$ to arithmetical comprehension, which is way beyond WKL$_0$.

*There is, however, something we can do to make the Skolem approach work reasonably well: consider explicitly Skolemized structures instead of general structures. An explicitly Skolemized model of a theory $T$ is a structure $A$ together with a family of Skolem functions corresponding to each axiom in $T$. It turns out that this is definable: there is a single formula $\eta$ such that in every universe $M$, $M\models\eta(T, A)$ iff $A$ is an explicitly Skolemized model of $T$ (where $T$ is a theory in $M$ and $A$ is a structure in $M$). This lets us define Skolem entailment: we write "$T\models_{skolem}\varphi$" iff $$\mbox{There is no explicitly Skolemized model of $T\cup\{\neg\varphi\}$}\}.$$ It should be noted however that this is a very non-constructive notion, for reasons which should be pretty obvious.

*Also, note that within a universe $M$ all these relations define collections of natural numbers which are externally sets but may not be sets within $M$ - this is just because $M$ may the necessary comprehension axioms to turn a definable collection of natural numbers into an actual set.

*Finally, of course, for any universe $M$ we can externally talk about the set of semantic consequences of a theory $T\in M$ in the sense of $M$: $T\models_\infty^M\varphi$ iff whenever $A\in M$ is a structure such that $A\models_n\theta$ for each $n$-quantifier sentence $\theta\in T$ we have $A\models_k\varphi$ where $\varphi$ has $k$ quantifiers. But in general this relation won't even be definable internally: there's no reason to believe even that the collection $\{\varphi: \emptyset\models_\infty^M\varphi\}$ is definable inside $M$.

Note that WKL$_0$ proves the completeness theorem in a very strong way: it proves "For every consistent theory $T$, there is an explicitly Skolemized model of $T$." This is basically the strongest version of the completeness theorem one can consider. Meanwhile, the statement "For every consistent theory $T$ consisting of sentences with at most $k$ quantifiers, there is a structure which $\models_kT$" implies WKL$_0$ for $k$ large enough (I think $k=3$ suffices). This is why the claim "WKL$_0$ is equivalent to the completeness theorem" isn't really misleading, even though there is a lot of technical subtlety around it.


OK, now on to an actual result to get us motivated:
As above, let $REC$ be the $\omega$-model of RCA$_0$ consisting of the recursive sets. In the context of $REC$, "valid" means "true in every recursive structure." Our journey begins with the observation that:
This might sound simpler, but it's actually more complicated!
This is a consequence of a particular version of Tennenbaum's theorem - that there is a single sentence $\alpha$ in the language of arithmetic, true in the standard natural numbers, which has no computable nonstandard models. (Tennenbaum's theorem is usually stated for PA, but holds for some appropriate finitely-axiomatizable theories too.)
We can now use $\alpha$ to reduce the true theory of arithmetic to validity: a sentence $\theta$ is true of $(\mathbb{N}; +,\times)$ iff $\alpha\implies\theta$ is valid in the sense of the model REC. Intuitively, what's going on here is that from the perspective of REC, $\alpha$ pins down the true natural numbers up to isomorphism.
Conversely, of course, the true theory of arithmetic can uniformly decide if a given first-order sentence has a computable model. So in the context of the model $REC$, validity is equivalent to arithmetic truth in a couple precise senses: 


*

*The (external) set $$\{\varphi: \emptyset\models_\infty^{REC}\varphi\}$$ has Turing degree $\bf 0^{(\omega)}$.

*For every sufficiently large $n$, the $REC$-definable class $$\{\varphi: \emptyset\models_n\varphi\}^{REC}$$ is not definable in $REC$ by a formula with fewer than $n$ quantifiers, and has external Turing degree $\bf 0^{(n)}$. (The "sufficiently large" is necessary since $\alpha$ itself has some number of quantifiers which we need to be allowed to use.)

Now $REC$ was a very special model; can we say something more general about how the failure of WKL$_0$ can affect the complexity of validity?
It turns out that we can - there is a very general theorem here which says roughly that the simplicity of validity is equivalent to WKL$_0$!

Theorem. Suppose $M$ is a universe in which WKL$_0$ fails - that is, there is an infinite binary tree $\mathcal{T}\in M$ with no infinite path in $M$. Then for all sufficiently large $k$ there is a theory $T_k$, consisting of sentences with at most $k$ quantifiers, such that the set of $\models_k$-consequences of $T_k$ is not $\Pi^0_{k-1}$-in-$T_k$-definable in $M$. Intuitively, semantic consequence is not arithmetical from the point of view of $M$. (By contrast, of course, the set of syntactic consequences of $T$ is definable in $M$ by a $\Sigma^0_1$-in-$T$ formula.)

The proof of the theorem above is a bit messy. One direction we already know. In the other direction, we're going to use the "impossible tree" $\mathcal{T}$ to pin down the standard model of arithmetic by a first-order theory $T$ computable in $\mathcal{T}$  (note that this is classically impossible by the compactness theorem). This will let us code Turing jumps of the (set coding the) tree $\mathcal{T}$ into validity questions, at which point the usual diagonalization arguments will preclude the possibility of a "simple" definition of validity.
In detail, we begin by letting $S_0$ be the following theory:


*

*The language of $S_0$ consists of a new constant symbol $c_\sigma$ for each $\sigma\in\mathcal{T}$, new unary predicate symbols $U_i$ for each $i\in\mathbb{N}$, and a new binary relation symbol $\triangleleft$.

*The axioms of $S_0$ consist of:


*

*"$c_\sigma\not=c_\tau$" whenever $\sigma,\tau\in\mathcal{T}$ are distinct.

*"$\triangleleft$ defines a (strict) partial ordering of the domain."

*"For all $x, y, z$, if $x\triangleleft z$ and $y\triangleleft z$ then either $x\triangleleft y, y\triangleleft x$, or $x=y$." That is, the set of things below a given element is linearly ordered by $\triangleleft$.

*"$U_i(c_\sigma)$" for every $\sigma\in\mathcal{T}$ of length $\ge i$.

*"$\forall x[\neg U_i(x)\iff \bigvee_{\sigma\in \mathcal{T}, length(\sigma)<i}x=c_\sigma]$" for every $i\in\mathbb{N}$. Note that this is in fact first-order, since there are only finitely many nodes on $\mathcal{T}$ of a given height.

*"$c_\sigma\triangleleft c_\tau$" for every $\sigma\prec \tau\in\mathcal{T}$, "$c_\sigma\not\triangleleft c_\tau$" for every $\sigma,\tau\in\mathcal{T}$ with $\sigma\not\prec\tau$.

*For each $i$, the axiom "For all $x$, if $U_{i+1}(x)$ holds then for some $y$ we have $y\triangleleft x$ and $U_i(y)\wedge\neg U_{i+1}(y)$."
It's now not hard to check that within $M$, $\Sigma$ has exactly one model up to isomorphism, namely the tree $\mathcal{T}$ itself with each node labelled appropriately; this is because any element of a model of $\Sigma$ not corresponding to an element of $\mathcal{T}$ yields an infinite path through $\mathcal{T}$, which doesn't exist in $M$. 
OK, next I'll consider a new theory $S_1$: 


*

*The language of $S_1$ consists of the language of $S_0$, together with the (disjoint) language of arithmetic, together with new unary relation symbols $A, B$ and a new binary relation symbol $E$. 

*The axioms of $S_1$ consist of:


*

*$A$ and $B$ partition the domain.

*$S_0$, relativized to $A$.

*(First-order) Peano arithmetic, relativized to $B$.

*$E\subseteq B\times A$. 

*For each $b\in B$ we have $bEa$ for some $a\in A$. 

*For each $i\in\mathbb{N}$ we have the axiom: for each $a_0, a_1\in A$, and $b\in B$, if $U_i(a_0)\wedge U_i(a_1)\wedge \neg U_{i+1}(a_0)\wedge \neg U_{i+1}(a_1)$ then $bEa_0\iff bEa_1$.

*For each $i\in\mathbb{N}$ we have the axiom: for each $b_0, b_1\in B$ with $b_0<b_1$ and each $a_0, a_1\in A$ with $b_0Ea_0$ and $b_1Ea_1$, $U_i(a_0)\implies U_{i+1}(a_1)$.
Intuitively, the last four axioms say that $E$ describes a map from the model of PA on the $B$-sort to the levels of the $A$-sort which is increasing (that is, smaller "numbers" get associated to smaller "levels"). By our analysis of $S_0$ above, we see that the model of PA attached to the $B$-sort is isomorphic to the standard model.
Now finally I'm ready to define $T$: it's the theory $S_1$, together with a new unary relation symbol $Z$ and axioms saying:


*

*$Z(s)$, whenever $s$ is (the numeral corresponding to) a natural number representing a node of $\mathcal{T}$.

*$\neg Z(s)$, whenever $s$ is (the numeral corresponding to) a natural number representing a node of $\mathcal{T}$.
By the usual coding arguments, for large enough $k$ the set of $k$-quantifier consequences of $T$ in the sense of $M$ is many-one equivalent in $M$ to the $k$th Turing jump of $\mathcal{T}$. Meanwhile, the theory $T$ itself is computable from $\mathcal{T}$, so this finishes the proof.
PHEW!

Let me end by stating what in my opinion are the two big open (as far as I know) questions along the lines indicated above:


*

*For which $\omega$-models $M$ of RCA$_0$ are there a natural number $k$ and a computable function $g$ such that $g$ is a many-one reduction from the set of indices for computable well-founded (as far as $M$ thinks) trees to $\{\varphi: \emptyset\models_k\varphi\}^M$? Basically, this is asking whether validity be (internally) $\Pi^1_1$ complete. Note that this is the "naive" upper bound on the complexity of validity. Note that $REC$ is such a model, since "well-foundedness" admits a $\Pi^0_3$ definition as far as $REC$ knows. But I'm interested in this phenomenon beyond $REC$, and in particular whether there is a nice characterization of this class of $\omega$-models.

*More open-endedly, I'd like a better understanding of how the complexity of validity can vary as we cause WKL$_0$ to fail in stronger or weaker ways (e.g. does WWKL$_0$ have anything to say on the matter? how about incomparable principles like RT$^2_2$?). 
I think the argument above is too "coarse" to be useful for either question, but I could be wrong; note that it only provided lower bounds on complexity. I'll think about these questions for a bit, and if I can't figure anything out I'll ask something at mathoverflow.
A: The problem is not building the model, it's making a completion of a theory.   This is related closely to the fact that the set of first-order valid formulas is semi-computable but not computable. 
Reverse Mathematics reveals this particular quirk of the completeness theorem. The following are in Simpson's book:

Theorem II.8.4, II.8.5 The following are provable in $\mathsf{RCA}_0$:
  
  
*
  
*Let $X$ be a consistent set of first-order sentences in a countable
  language so that $X$ is closed under logical consequence. Then there 
  exists a countable model of $X$.
  
*Let $X$ be a consistent set of first-order sentences in a countable language so that $X$ is closed under logical consequence. Then there exists a theory $X^* \supseteq X$ so that $X^*$ is complete and consistent and closed under logical consequence.  

and

Theorem IV.3.3. The following are: equivalent to $\mathsf{WKL}_0$ over $\mathsf{RCA}_0$. 
  
  
*
  
*Completeness theorem: If $X$ is a consistent set of first-order sentences in a countable language then there is a countable model of $X$. 
  
*Lindenbaum's lemma: If $X$ is a consistent set of first-order sentences in a countable language then $X$ has a completion, that is, a consistent, complete theory containing $X$ closed under logical consequence. 

This means there is a hidden side effect of the definitions and of the completeness theorem. The theory of a model is always complete, consistent, and closed under logical consequence. But a given set of axioms for a theory may be consistent but not complete and not closed under logical consequence.   
So, when our definitions say that a model comes equipped with a satisfaction relation, this means that the completeness theorem implies "every consistent countable theory has a completion to a consistent, complete, consistent theory closed under logical consequence".  We may not be able to find any such completion effectively, but this is the only non-effective step required in the proof. 
This is why $\mathsf{WKL}_0$ is required for the completeness theorem. If we only applied the completeness theorem to theories that were already closed under logical consequence, we would not need $\mathsf{WKL}_0$ at all, and in fact each such theory has a model computable from the theory. 
A: Although it is the case that the Completeness Theorem of First Order Logic implies that : 
Every valid sentence $\varphi$ has a proof.
and that such proofs can be found semi-decidably - there is a sense in which the necessity of using weak Konig's Lemma ($WKL_{0}$) in the meta-proof of the Completeness Theorem (and also of the Compactness Theorem) allows one to construct a Logic of First Order expressivity being incomplete and non-compact. This will happen when the semantics is constructive, unlike in First Order Logic.
An interesting example is Herbrand Logic from the Stanford Logic Group. 
Here there is a replacement to the semantics is as schematically described:
First Order Logic == First Order Syntax + Tarski Semantics
Herbrand Logic ==    First Order Syntax + Herbrand Semantics
Herbrand Semantics is constructively determined from the syntax itself, and does not need $WKL_{0}$ to construct arbitrary models. In Herbrand Logic entailment is not semi-decidable, the logic is inherently incomplete, and non-compact. 
Some valid statements would require infinite proofs.
There are some simple examples, although the formal meta-proof uses Diophantine Sets.
