Not Understanding a Move in Henkin Completeness Proof

[MLP]

Let L be a first order language. Let A be any set of sentences of L. We extend L0 (=L) to L1 by adding denumerably many constants c1, …,cn,… to L. We enumerate the existential formulas of L. We add Henkin axioms to L by taking each formula in the enumeration and making it the antecedant of a conditional whose consequent is an instantiation of the existential variable in the antecedent to the next earliest constant in the enumeration c1, …,cn,…

Up to here I think I get it. I have an extended system such that any existential claims entailed by the formulas in A, together with the appropriate Henkin axioms will yield instances of the existential claims via what I have seen called "witnessing constants". What I'm failing to see is why I need to go on? Once I have L1, why not just construct my model of L1? I am not understanding the move to add another set of constants and Henkin axioms, and then another, and so on to get L2,L3,etc.?

I'm sure I'm missing something obvious.

 

[Preno]

I'm sure I'm missing something obvious.

Yes, namely that quantifiers can be nested.

For example, take the sentence \exists x (P(x) \wedge \exists y R(x,y)). \exists x (P(x) \wedge \exists y R(x,y)) \rightarrow (P(c_1) \wedge \exists y R(c_1,y)) is its Henkin axiom. To get rid of the quantifier binding the y variable, you have to add another Henkin axiom for the sentence \exists y R(c,y): \exists y R(c_1,y) \rightarrow R(c_1, c_2). But this sentence already includes the Henkin constant c_1, so the constant c_2 is not in L1. You need an infinite hierarchy of Henkin constants to deal with nested quantifiers of arbitrary depth. Only then can you reduce an arbitrary sentence to a propositional level.

 

[MLP]

Thank you that was it!