Relation between algebraic geometry over a field of characteristic $0$ and that over $\mathbb{C}$ Let $K$ be an algebraically closed field of characteristic $0$.
Let $P$ be a proposition on a non-singular projective variety over $K$ which is stated in the language of algebraic geometry.
Suppose $P$ holds when $K = \mathbb{C}$.
Does $P$ hold on any such $K$?
Remark
We may take as $P$, for example, the Kodaira vanishing theorem.
 A: The Lefschetz principle can be understood in scheme theoretic terms in the following way:
suppose that $X \to S$ is a scheme over a base $S$ (possibly with extra data) which is fppf over $S$.  Then we may descend $X$ to $X_0 \to S_0$ where $S_0$ is finite type over $\mathbb Z$.  (Here "descend" means that there is a map $S\to S_0$ so that $X$ is recovered from $X_0$ via base-change.  For a proof/explanation, search for discussions of "removing Noetherian hypotheses" online.  The standard reference is somewhere in EGA IV.)
Now suppose that $P$ is a property that can be checked after faithfully flat base-change; then we use the above method to tranfer $P$ from the context of complex scalars to any field of char. zero.
E.g. if $(X,\mathcal L)$ is a smooth projective variety over a field $k$ of char. zero, then via the above we may descend $(X,\mathcal L)$ to $(X_0,\mathcal L_0)$ over a finite type $\mathbb Z$-scheme $S_0$.  The morphism Spec $k \to S_0$ factors as Spec $k \to $ Spec $k_0 \to S_0$, where $k_0$ is a finitely generated subfield of $k$, since $S_0$ is finite type over $\mathbb Z$.  Base-changing to $k_0$, we get $(X_0',\mathcal L_0')$ over $k_0$ which recovers $(X,\mathcal L)$ after base-changing to $k$.
Now choose an embedding $k \to \mathbb C$, as we may do since $k_0$ is finitely generated.  Base-change to $\mathbb C$ gives $(X',\mathcal L')$.
So we have $(X,\mathcal L)$ and $(X',\mathcal L')$ over $k$ and over $\mathbb C$, both of which are base-changed from $(X_0',\mathcal L_0')$ over $k_0$.
Using the fact that properness, smoothness, and ampleness may be checked after a faithfully flat base-change (in our case, just a change of base field), and are also preserved by such a base-change, and also that formation of the canonical bundled, and of cohomology, also commutes with change of base field, we can transfer Kodaira embedding from $(X',\mathcal L')$ to $(X_0',\mathcal L_0')$, and finally to $(X,\mathcal L)$, as desired. 
Note: The fact that $X\to S$ can be recovered from $X_0\to S_0$ is one way of encoding Lefschetz's intiuition that an algebraic variety only requires a finite amount of data to encode, which is what underlies the Lefschetz principle.  In practice, people use this a lot, whereas I've never seen anyone use a logical or model-theoretic formulation of the Lefschetz principle in an algebraic geometry argument.
People also use the closed points of $S_0$, which have positive characteristic, to deduce facts about the original $X$ --- thus the decomposition theorem for perverse sheaves in char. zero was first proved by such reduction to char. $p$ methods, as was the bend-and-break lemma in the theory of birational geometry.  Raynaud gave a proof of Kodaira embedding by proving it first in a char $p$ setting and then passing to char. $0$ by these methods.  In the context of passing from char. $p$ to char. $0$ there also more model-theoretic arguments, such as in some proofs of  the Ax-Grothendieck theorem, but my experience in this context too is that "spreading out" arguments (people call the passage from
Spec $k$ of char. zero to $S_0$ "spreading out" over $\mathbb Z$) are much more common.
A: You will have to restrict the language, obviously, because $P$ could be the proposition "the base field is $\mathbb{C}$". As André Nicolas has already mentioned, if $P$ is a proposition in the first-order language of fields then anything that holds for $\mathbb{C}$ holds for any algebraically closed field of characteristic $0$. This, however, is much less impressive than it sounds: first-order logic cannot express many things we take for granted like "there are uncountably many elements". 
However, there are more powerful results from model theory that give stronger transfer principles. Hodges [Model theory, §A.5] writes:

Finally there is an old heuristic principle which Weil [1946] called Lefschetz' principle. According to Weil (p. 242f),

… for a given value of the characteristic $p$, every result, involving only a finite number of points and varieties, which can be proved for some choice of the universal domain … is true without restriction; there is but one algebraic geometry of characteristic $p$, for each value of $p$, and not one algebraic geometry for each choice of the universal domain. In particular, as S. Lefschetz has observed on various occasions, whenever a result, involving only a finite number of points and varieties, can be proved in the ‘classical case’ where the universal domain is the field of all complex numbers, it remains true whenever the characteristic is $0$ …

This looks as if it should be a model-theoretic principle, and several writesr have suggested what model-theoretic principle it might be. The most convincing proposals are those of Barwise & Eklof [1969] using $L_{\omega_1 \omega}$, and of Eklof [1973] using $L_{\infty \omega}$; [...]

So what exactly do the cited results say? First things first: $L_{\infty \omega}$ refers to the language of infinitary first-order logic, i.e. the logic where conjunctions and disjunctions of arbitrary sets of formulae are allowed, but only any string of consecutive quantifiers is finite. $L_{\infty \omega}$ is more expressive than finitary first-order logic (known as $L_{\omega \omega}$ in symbols): it is possible to express in $L_{\infty \omega}$ (with the help of sufficiently many constant symbols) the proposition "there are most $\kappa$ elements", for any cardinal $\kappa$. This is known to be impossible in $L_{\omega \omega}$ when $\kappa$ is any infinite cardinal, essentially by the upward Löwenheim–Skolem theorem. $L_{\omega_1 \omega}$ is the fragment of $L_{\infty \omega}$ where only countable conjunctions and disjunctions are allowed. We say that two structures are $L_{\infty \omega}$-equivalent if they satisfy exactly the same sentences over $L_{\infty \omega}$. 
Now let $\mathcal{C}$ be the category of structures for a many-sorted first-order signature $\Sigma$, with $\Sigma$-homomorphisms as the morphisms of $\mathcal{C}$. (As usual this means a map that preserves the interpretation of function symbols and relation symbols in $\Sigma$.) An embedding is an injective homomorphism that reflect the interpretations of the relation symbols in $\Sigma$. Let $\mathcal{U}_p$ be the category of universal domains of characteristic $p$. An $\omega$-local functor $F : \mathcal{U}_p \to \mathcal{C}$ is a functor satisfying these conditions:


*

*The image under $F$ of any homomorphism in $\mathcal{U}_p$ is an embedding in $\mathcal{C}$.

*Given a field extension $U' \subseteq U$ in $\mathcal{U}_p$ and any finite subset $X$ of $F U$, we can find an intermediate extension $U' \subseteq U'' \subseteq U$ in $\mathcal{U}_p$ such that $U''$ is of finite transcendence degree over $U'$, and if $j : U'' \hookrightarrow U$ is the inclusion, $X$ is contained in the image of $F U''$ under $F j$. 


It turns out that a functor $F : \mathcal{U}_p \to \mathcal{C}$ is $\omega$-local if and only if it preserves directed colimits (and so if and only if it preserves filtered colimits; see [Adámek and Rosický, LPAC, Thm. 1.5]). Eklof's 1973 result is the following:
Theorem. If $F : \mathcal{U}_p \to \mathcal{C}$ is an $\omega$-local functor, then $F U_1$ is $L_{\infty \omega}$-equivalent to $F U_2$ for any $U_1$ and $U_2$ in $\mathcal{U}_p$.
To apply this to algebraic geometry, we take $F$ to be the functor that takes a universal domain $U$ to the fragment of "geometry" we are interested in; for example, we could take $A = F U$ to have the following elements:


*

*$A_0$ is the set of integers.

*$A_1 = \bigcup_{n < \omega} U^n$ is the union of all finite-dimensional affine spaces over $U$.

*$A_2 = \bigcup_{n < \omega} U [x_1, \ldots, x_n]$ is the union of all finitely-generated polynomial rings over $U$.

*$A_3 = \bigcup_{n < \omega} \{ I \triangleleft U [x_1, \ldots, x_n] \}$ is the set of all ideals over all finitely-generated polynomial rings over $U$.

*$A_4$ is the set of affine varieties in $U$ (concretely realised as subsets of $A_1$, I suppose).

*$A_5$ is the set of abstract varieties. (There is only a set of them because each one is covered by finitely many open affine subvarieties.)

*etc.


The relations of $A$ will be those expressing the propositions of interest; for example, we could have a relation that encodes the proposition "$V$ is an $n$-dimensional variety", where $V$ is a variable of type $A_5$ and $n$ is a variable of type $A_0$. These should be chosen so that $F$ actually defines a functor, i.e. so that extending the universal domain doesn't change the truth value of the propositions of interest. Then Eklof's theorem tells us that all of these "geometries" are $L_{\infty \omega}$-equivalent: in essence, it tells us that the propositions of "geometry" that are independent of the choice of universal domain are those preserved by extension of universal domain, and the class of these propositions is closed under a rich class of logical connectives.
