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?