I take Bézout's theorem to be the statement that given two different irreducible algebraic curves in two-dimensional projective space over an arbitrary field $K$, of degrees $m$ and $n$, the number of points of intersection does not exceed $mn$.
The only proof I know assumes that $K$ is infinite, so that via a projective transformation you can prevent $[1,0,0]$ from sharing the same line with any pair of distinct points of intersection.
Could I prove the same theorem in a more restricted language: perhaps one in which the infinite size of $K$ or the possibility of field extensions cannot be expressed?
I'm confused about what you're looking for. You state a version of Bézout's theorem in a way that applies to an arbitrary field:
For clarity, I'll call this statement Bézout's theorem. You say that you only know how to prove this for infinite fields. That's fine. Here's where I get confused:
It doesn't really matter whether a language can express the infinite size of $K$, does it? What matters is whether your proof uses the assumption that $K$ is infinite. And since the proof you have in mind uses this assumption, it's not a proof of the full statement of Bézout's theorem, and it can't be used to "automatically" give a proof.
Of course, Bézout's theorem is true for arbitrary fields. Here's a proof that bootstraps from your proof. Fix two irreducible algebraic curves in two-dimensional projective space over an arbitrary field $K$. Embed $K$ in its algebraic closure $\overline{K}$. Now $\overline{K}$ is infinite, so by your proof, the number of points of intersection in $\mathbb{P}^2(\overline{K})$ is at most $mn$. But every point of intersection in $\mathbb{P}^2(K)$ is also a point of intersection in $\mathbb{P}^2(\overline{K})$, so $mn$ is also an upper bound over $K$.
It seems like you were looking for some kind of abstract "logical" approach to transferring the result from infinite fields to arbitrary fields... one way to view the proof I gave above is to observe that Bézout's theorem can be stated as a family of universal sentences (sentences of the form $\forall \overline{x}\, \varphi(\overline{x})$, where $\varphi(\overline{x})$ is quantifier-free) in the first-order language of fields, one sentence for each pair of degrees $(m,n)$. Now universal sentences are preserved under substructure: e.g. if a universal sentence is true in some field, it's automatically true in any subfield. Since every field is a subfield of an infinite field, the statement of Bézout's theorem transfers from infinite fields to arbitrary fields.