The question is about the proof of Lemma 6.7 in Yuri Manin's "A Course in Mathematical Logic", which is part of the proof of Gödel's completeness theorem.
Lemma 6.7 If $\mathcal{E}$ is consistent and contains $\text{Ax }L$, then there exist:
(a) a language $L'$ whose alphabet is obtained from the alphabet of $L$ by adding a set of new constants having cardinality $\leq$ card (alphabet of $L$) + $\aleph_0$.
(b) a set of formulas $\mathcal{E'}$ in $L'$ which is consistent, contains $\mathcal{E}$ and $\text{Ax }L'$, and has the property that the alphabet of $L'$ is sufficient for $\mathcal{E'}$.
Part (a) of the claim is proven by simply adding to the alphabet of $L$ a set of new constants of cardinality card (alphabet of L) + $\aleph_0$, and creating a new language $L'$ using this alphabet. The proof then shows that $\mathcal{E} \cup \text{Ax }L$ is consistent, and I am okay with this part.
This particular section of the proof is confusing:
(c) We consider the set $S$ of formulas $P(x)$ containing one free variable $x$ and such that $\neg\forall x P(x) \in \mathcal{E} \cup \text{Ax }L'$. For each $P(x)$ in $S$ we choose a new constant $c_P$ subject to the following restriction: each $c_P$ can be assigned a natural number, its rank, in such a way that if a constant of rank $n$ occurs in $P(x)$ then $c_P$ has rank $\gt n$.
The set $\text{Ax }L'$ consists of the tautologies of $L'$ and logical quantifier axioms. But a proposition of the form $\neg\forall x P(x)$ cannot be either of those.
It cannot be a tautology because tautologies are logical polynomials over a finite set of base propositions, whose truth value is $1$ independently of the choice of truth value for each base proposition (section 3.4). Since $\neg\forall x P(x)$ contains only a single connective $\neg$ (quantifiers cannot show up as connectives), either $\neg\forall x P(x)$ or $\forall x P(x)$ must be the base proposition, and clearly in both cases the truth value is dependent on the truth value of the base proposition.
The formula $\neg\forall x P(x)$ cannot either be a logical quantifier axiom because the quantifier axioms have one of the following structures, none of which fit the structure of $\neg\forall x P(x)$ (section 3.5):
(a) $\forall x (P \implies Q) \implies (P \implies \forall x Q)$
(b) $\forall x \neg P \iff \neg \exists x P$
(c) $\forall x P(x) \implies P(t)$
Therefore we must have "$\neg\forall x P(x)$" $\in \mathcal{E}$. But in that case, there cannot be any new constants $c_P$ of $L'$ contained in that formula since it lies in the original language $L$ which does not have this extended alphabet.
With that reasoning, it would seem that the rank of $c_P$ can always be chosen as $1$, because there are no constants of rank $\geq 1$ contained in $P(x)$. So the notion of "rank" seems to be useless for the proof.
Did I miss something which makes it essential to introduce the rank, or can the proof carry on without it?