Can the Completeness Theorem be proven constructively in a natural-deductive system?

Question

In Sets, Logic and Computation the following is said of the Completeness Theorem:

When completeness is thought of as “whenever $\models A$ then $\vdash A$,” it may be hard to even come up with an idea: for to show that $\vdash A$ we have to find a derivation, and it does not look like the hypothesis that $\models A$ helps us for this in any way. For some proof systems it is possible to directly construct a derivation, but we will take a slightly different approach.

I'm interested, first of all, what these systems are in which it is possible to construct such a proof. Secondly, though, I'm curious if this is translatable to natural deduction. In particular, I'm curious if there are any texts which prove this statement constructively, preferably in Fitch notation.

Answer 1

What I had in mind was simply that some proof systems lend themselves to systematic proof search which, if $\models A$, is guaranteed to be successful. E.g., in sequent calculus LK, you basically apply the rules in reverse, and if you do it systematically (in particular, apply the strong quantifier rules often enough), you eventually find a derivation. This is the basis of the direct completeness proof for LK, I believe first due to Schütte. Completeness is proved this way in Takeuti's proof theory book; I'm sure there are more readily available references but none come to mind off the top of my head. As @Mark Savig mentioned, any such derivation in the sequent calculus LK can be translated into one in natural deduction or Hilbert-style systems. You can do systematic proof search in natural deduction directly as well, but Fitch-style is not the best notation to do that in. But essentially the "proof construction strategies" in intro textbooks that use Fitch-style proofs are such proof search methods.

(Asides: 1. Putting this as "it is possible to construct a derivation" is perhaps misleading as this question shows; I'll clarify this in the text. 2. The Henkin-style completeness proof essentially also includes such a proof search procedure, but the proof obscures this. Basically, if your set is inconsistent, the Lindenbaum construction will fail to produce a maximally consistent set, and the derivation of an explicit contradiction from some stage $\Gamma_i$ will give you a derivation of a contradiction from the starting set $\Gamma$. But that is very roundabout. 3. Proof search is possible for every proof systems where the derivations are computably enumerable, and is guaranteed to terminate if the system is complete. But that it is complete can't be shown this way except if you can construct a countermodel from an infinite failed proof search, like in Schütte's proof. And this requires some non-constructive principle such as WKL.)

Answer 2

First, it is easy to show that natural deduction systems prove exactly the same sentences as Hilbert systems. This is a purely syntactic fact and can be proved constructively. It is therefore straightforward to conclude the completeness theorem applies to one of these deductive system if and only if it applies to the other. Most of the standard proofs of the completeness theorem should be easily translated to natural deduction systems; I’m hard-pressed to think of one that wouldn’t.

Second, the completeness theorem cannot be proved constructively. In fact, it cannot even be proved in ZF; over ZF, it is equivalent to the ultrafilter lemma (and a great many other things besides), which is independent of ZF.