My question concerns Henkin's original (1950) completeness proof in Completeness in the theory of types 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 in The completeness of the first-order functional calculus.
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 Completeness in the theory of types, 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 $\textbf{M_0}$ such that $\vdash (\exists x_b)M_0$, then we also have $\vdash (\lambda x_b. \textbf{M_0 }) (\iota_{b,(0b)}(\lambda x_{\beta}.\textbf{M_{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 $\mathscr{T}$, 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 $\iota{b(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)?
