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? 



Possible to prove a lemma from Godel's completeness theorem in intuitionistic logic?
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*](http://www.andrew.cmu.edu/user/avigad/Papers/goedel.pdf), and notes afterwards:



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


