mjhjmtu

My question concerns Henkin's original (1950) completeness proof https://projecteuclid.org/euclid.jsl/1183730860 for classical higher order logic and type theory relative to so-called general models.

His 1950 proof seems quite different to his (1949) completeness proof of first order logic https://projecteuclid.org/euclid.jsl/1183730666.

In particular, the 1950 completeness proof for classical type theory does not, at first sight, seem to employ the famous construction whereby the language is expanded by adjoining constants to it thereby providing witness to existential formulae, whereas his 1949 completeness proof does. (The main body of his 1950 proof is on p.85-88 of https://projecteuclid.org/euclid.jsl/1183730860, which constructs a maximally consistent set of formulae, but surprisingly does not mention constants and their role as witnesses for existential formulae)

I mentioned this to a colleague who expressed surprise/incredulity that the completeness proof for classical type theory does not employ this construction. He suggested that it might be hidden somewhere in the proof, and that perhaps the $iota$ operator employed by Henkin plays the role of supplying fresh constants with which to witness existential formulae.

Indeed, it is clear from Henkin's comments in that he views the $iota$ as playing an important role in the completeness proof, and this passage suggests he views it as a way of providing witnesses for existential formulae:

"The very first question I asked myself was whether I could use the method
that gave me completeness for type theory, to get a new proof of Godel's
completeness for first-order logic. It seemed, at first, that there was no
possibility to do so. The reason is that the axiom of choice, and in particular Church's neat formulation of it via the constants $i_a(Oa)$, played a crucial role in the proof for type theory, while in first order logic there is no axiom of choice, and no way to formulate one.
I decided to analyze carefully the role of the axiom of choice in the completeness proof, to see whether there was some other way of accomplishing it in first-order logic. The role that I saw first was performed in the proof by induction, sketched above, that domains $D_alpha^'$ satisfying conditions (i)-(iii), could be constructed. But when I wrote down details of the proof that the resulting hierarchy of domains $D_alpha^'$ satisfy the maximal consistent set of (added) axioms, I saw that the axiom of choice is needed there in a more general way, of which the earlier use is just a special case. The more general need is to show that whenever we have a wff $textbfM_0$ such that $vdash (exists x_b)M_0$, then we also have $vdash (lambda x_b. textbfM_0 ) (iota_b,(0b)(lambda x_beta.textbfM_0))$. The fact that this condition holds is a direct consequence of having Axiom Schema $11^b$ in the deductive system that Church had set up for the theory $mathscrT$, as that schema is trivially equivalent to $(exists x_b f_0b x_b) supset f_0b(iota_b(0b) f_0b)$...I did not altogether hide the symbols $i_b(0b)$ from the reader of my dissertation,
for in passing from Theorem VI to Theorem VII, in which the
generalized completeness theorem is extended to languages that can be nondenumerable or have additional constants, I cited Church's system in which the axiom schemas of description and choice are formulated with the symbols $iotab(0b)$, as an example. With that example is a brief note to the effect
that when this formulation of the axiom of choice is made, the adjunction of special constants $u_b, u_b^', u_b^'',...$ for each type symbol $b$ becomes unnecessary in the completeness proof, as their role can be taken over by the symbols $iota_b(0b)$. Still, it would be a very sharp-eyed historian who could detect in that brief note appended to Theorem VII, the origin of the proof of Theorem I!" (from http://www2.mat.ulaval.ca/fileadmin/Cours/MAT-10391/Henkin_BSL_1996.pdf)

So is my colleague right about this?

Does the 1950 proof implicitly contain the relevant construction?

$Edit$:

The mystery is made worse by the fact that Henkin in his 1949 paper writes that his proof "suggests a new approach to the problem of completeness for functional calculi of higher order" to be "taken up" in a further paper (presumably his 1950 paper). In the 1950 paper he writes (ft6, p.82) that a completeness proof of second order logic relative to general models "can be carried out along the lines of the author's recent paper" (i.e his 1949 paper). So what precisely is the link between the earlier paper and the later (presuming it is not the famous construction involving adjoining constants to the language)?

Henkin's completness proof for first order logic (using his method of constants) and Henkin's work on the completeness of type theory were both carried out in his doctoral 1947 dissertation written under the direction of Alonzo Church. The dissertation was never published, but Henkin wrote a fascinating and detailed article about the genesis of the intertwining ideas in his thesis in 1996 (The Discovery of My Completeness Proofs, The Bulletin of Symbolic Logic, Vol. 2, No. 2 (Jun., 1996), pp. 127-158).

The following quote from the above paper (starting in the bottom of page 154 and continued to the next page) seems to answer your question (and vindicate your colleague). Henkin uses "cwff" for closed well-formed formulae; i.e., those with no free variables.

As indicated, in addition to putting the first-discovered proof into Part
III of the dissertation, I hid the discovery process in another way. Namely,
in setting forth the formal language for type theory, in Part III, I deleted
from Church's system the symbols $iota_b(0b)$ and the axiom of choice for which they were used! Those symbols, and that axiom, which quintessential role in the discovery process, were omitted in Theorem VI, and the role of the symbols $iota_b(0b)$ in forming "witnesses" cwffs of the form $exists x_bM_0$ was taken over by the adjunction of constants $u_b$, $u'_b$, $u''_b$ for each type symbol $b$.