Possible to prove a lemma from Godel's completeness theorem in intuitionistic logic?

I am trying to determine whether a particular theorem used in the course of Godel’s (1930) proof of the completeness of predicate logic could be proven in an intuitionistic metatheory.

Theorem VI (p. 113 of Godel Collected Works, Vol. I) states that:

For every n,

$$P(A) \implies P_n(A_n)$$

is provable in the system, where $$P(A)$$ is a normal form formula of first-order predicate logic, and $$P_n(A_n)$$ is the existential closure of the nth “expansion” of A. The expansions $$A_i$$ of $$P(A)$$ are constructed by systematically replacing the r-many universal variables of $$P(A)$$ by r-tuples in some pre-given ordering, and for each r-tuple, adding n-many new indexed variables to replace the existential variables of $$P(A)$$.

The proof appeals to several lemmas and rules of inference involving quantifiers. Most of these involve renaming of variables and do not seem intuitionistically problematic to me. However, Lemma 1(a) allows one to infer $$\exists x_1, x_2,...x_r F (x_1, x_2,...x_r)$$ from $$\forall x F (x_1, x_2,...x_r)$$. This seems problematic to me, since it permits an existence statement to be made without giving the means of construction for those $$x_i$$.

I am not sufficiently familiar with Herbrand’s work, but I know he was operating within a “finitistic” (read: intuitionistic) framework. I suspect that he needs to prove some equivalent to Theorem VI in order to prove his Fundamental Theorem. Can anyone confirm whether Theorem VI can be proved in an intuitionistic metatheory or, if not, where the relevant step might occur in Herbrand’s proof?

• From $\forall x\, F(x)$ we can infer $\exists x\, F(x)$ by taking $x=1$ — that’s not problematic. Sep 30 '19 at 5:08
• @MattF.: Do you mean semantically, or syntactically? In either case, it depends on having “1” available as a value the variables can be given. Semantically, that is available in Gödel’s paper, because he points out that according to “well-known theorems” all models can be assumed to have domain $\mathbf{N}$. Syntactically, it’s not true in Gödel’s setting, since the language of his object theory doesn’t include a symbol “1”, if I understand it correctly. Your main point is right, though — as long as we have some value $x$ can be given, there’s nothing un-intuitionistic about this lemma. Sep 30 '19 at 15:33

Lemma 1(a) is about derivability of $$\newcommand{\x}{\mathbf{x}}\forall \x\, \varphi(\x) \Rightarrow \exists \x\, \varphi(\x)$$ in the object theory, not the metatheory.

Gödel doesn’t give the proof, but it’s nothing subtle: in the deduction system he considers, and many similar systems, you can just write down the derivation, uniformly in the formula $$\varphi$$. So if the object theory you’re considering is the same as in Gödel’s paper, then regardless of your metatheory, this lemma is unproblematic.

On the other hand, many modern presentations of logic (even classical logic) don’t prove $$\forall \x\, \varphi(\x) \Rightarrow \exists \x\, \varphi(\x)$$. In a classical metatheory, the completeness theorem goes through quite happily for such systems; one just has to use slightly different intermediate lemmas.

(The given formula is known as existential commitment, and corresponds to the semantic restriction that all structures must have non-empty domain. Syntactically, the traditional proof is a two-liner, in suitable natural deduction systems: take arbitrary variables $$\newcommand{\y}{\mathbf{y}}\y$$ (or terms); then go from $$\forall \x\, \varphi(\x)$$ to $$\varphi(\y)$$ by $$\forall$$-elimination, and onward to $$\exists \x\, \varphi(\x)$$ by $$\exists$$-introduction. However, this relies on variables always being available as terms. More careful versions of natural deduction keep track of the scope or context of derivations. Then over the empty context, there are no variables in scope, and so if the language in consideration doesn’t have constant symbols, there are no terms in scope to use $$\forall$$-elimination on. So in such systems, $$\forall \x\, \varphi(\x) \Rightarrow \exists \x\, \varphi(\x)$$ is not derivable over the empty context, and the proof system is sound for arbitrary structures, without a restriction to non-empty domains. I firmly hold the view that the latter systems are more natural, and give a better theory; that the popularity of systems proving $$\forall \x\, \varphi(\x) \Rightarrow \exists \x\, \varphi(\x)$$ is an unfortunate historical accident, which happened because these systems got widely accepted and standardised before a good machinery for handling scopes/contexts had been developed.)

In summary, Lemma 1(a) is about the object theory, not the meta-theory; moreover, it is about the existential commitment of the object theory, not about whether it’s classical or intuitionistic.

Relevantly, Jeremy Avigad gives a very nice presentation of Gödel’s completeness proof from a modern viewpoint, in section 4 of his 2006 article Gödel and the metamathematical tradition, and notes afterwards:

…the constructive content is clear; the only nonconstructive element is the use of König’s lemma in step 2.

• The key term here is free logic: plato.stanford.edu/entries/logic-free Oct 1 '19 at 0:15
• @FrançoisG.Dorais: Right, I considered mentioning that term, but didn’t since I find its use for this specific feature misleading. The work I’ve seen using the term “free logic” emphasises its differences from established classical systems; which is great when it looks at genuinely substantive differences (like having terms with no denotation), but then a bit silly for discussing this comparatively trivial feature, which (to me, and I think most others at least in the categorical logic/type theory traditions) is just fixing a minor wart of the traditional presentation. Oct 1 '19 at 0:42
• Peter, I didn't realize it was anything but a minor wart to anyone! Oct 1 '19 at 2:24