Why k- Vertex Cover is not in PTIME when it can be expressed in FO-logic

We can express property that graph has vertex cover of size at most k with first order formula:

$$\exists x_1 \exists x_2...\exists x_k (\forall y \forall z (E(z,y) \ \rightarrow \ \bigvee_{1 \leq i \leq k} y=x_i \ \vee \ \bigvee_{1 \leq i \leq k} z=x_i))$$

But, there is also theorem (proven for example in Libkin's book Finite model theory) that for every given FO sentence and finite model A one can decide does:

$$A \models \varphi$$

in PTIME.

Why can't we use this for sentence expressing k-VC property, written above, and decide does any given graph has this property?

Your argument shows that for each fixed $k$, the problem $k$-VC can be solved in polynomial time (indeed, the algorithm enumerates all sets of size $k$ and checks whether they are vertex covers, all of which can be accomplished in $O(n^{k+1})$ or so). However, the vertex cover problem is different – it accepts $k$ as an input. This version of the vertex cover problem cannot be expressed in first-order logic.

StackExchange Computer Science Q#81360, answer score: 7