The terms "local" and "global" when applied to large cardinal axioms seem to have a well understood intuitive meaning, although a formalized definition of them in (a metalanguage for)ZFC might be quite unwieldy. Given a large cardinal axiom, set theorists can immediately classify it as local or global. Loosely speaking, it is local iff you do not have to "look at" sets of arbitrarily high rank in the set theoretic hierarchy to determine whether the axiom does or does not hold. I have often wondered whether any global large cardinal can ever be "smaller" than some local large cardinal. I have never seen a statement that this is not possible. But is it? To be more specific: Is there any example of a local large cardinal axiom L, such that a sentence which states that the smallest supercompact cardinal is smaller than the smallest cardinal satisfying Lis not known to be inconsistent with ZFC? We always assume, of course, that the conjunction of both axioms holds.

I don't agree that it is difficult to formalize the local/global distinction, and indeed, I think that there is a largely agreedupon technical meaning for these notions. Specifically, a property is locally verifiable if it can be verified inside any sufficiently large rank initial segment $V_\theta$ of the universe. So $\varphi(x)$ is such a property if it is equivalent to $\exists\theta\ V_\theta\models\psi(x)$, for some assertion $\psi$ (of any complexity). It is an excellent exercise to prove that the local properties are precisely the $\Sigma_2$ expressible assertions. To be truly local, both the property and its negation should be locally verifiable, which would make the property $\Delta_2$. Update: I have posted further discussion of this issue on my blog at Local properties in set theory, including a proof of the equivalence I mentioned above. Examples of local large cardinal properties would include inaccessible, Mahlo, weakly compact, Ramsey, measurable, Woodin, superstrong, almost huge, huge, rankintorank and many others. In particular, some local large cardinal properties are extremely high in the large cardinal hierarchy. Global properties, in contrast, are not verifiable inside any particular $V_\theta$, and most of the commonly considered global large cardinal properties have complexity $\Pi_2$ or $\Pi_3$. For example, $\kappa$ is supercompact if and only if for every $\lambda$ it is $\lambda$supercompact. For any particular $\lambda$, the assertion that $\kappa$ is $\lambda$supercompact is local, since it can be verified inside $V_{\lambda+3}$ or so, and so it is $\Sigma_2$. The universal quantifier in front would seem to make supercompactness a $\Pi_3$ property, but actually it is $\Pi_2$, since the failure of the supercompactness of $\kappa$ is locally verifiable, as $\kappa$ fails to be supercompact just in case this is true inside some tall enough $V_\theta$ (thanks to Kostas for his comment on my blog about this, and he says it is mentioned also in Kanamori Ch. 5 after exercise 22.8). Other global large cardinal properties include: uplifting, strongly uplifting, unfoldable, strongly unfoldable, tall, strong, strongly compact, supercompact and many others. Some of the global properties occur very low in the large cardinal hierarchy. For example, the uplifting cardinals are weaker than Mahlo in consistency strength, yet they are not local properties. So there are numerous instances where a global property has weaker consistency strength than a local property. Meanwhile, however, every supercompact cardinal (and every strong cardinal) is $\Sigma_2$reflecting, and therefore if there is any typeL large cardinal above $\kappa$, then there would have to be many below $\kappa$. So the least supercompact cardinal can never be less than the least $L$cardinal, if $L$ is a local property. 


Based on Monroe's comment, I've expanded my comment into an answer: A strongly compact cardinal is a $\kappa$ such that every $\kappa$complete filter $F$ on $\kappa$ can be extended to a $\kappa$complete ultrafilter. (Note that this trivially implies that $\kappa$ is measurable: take $F=\{\kappa\}$.) This seems to me to be a local property. Of course, ultrafilters are closely connected with elementary embeddings, which are global objects; but to me at least strong compactness is as local as measurability. A Woodin cardinal is a $\lambda$ such that for every $f:\lambda\rightarrow\lambda$, there is $\gamma<\lambda$ such that $f"\gamma\subseteq\gamma$ and an elementary embedding $j: V\rightarrow M$ with critical point $\gamma$, satisfying $$ V_{j(f)(\gamma)}\subseteq M.$$ Although this quantifies over only elements of $\lambda^\lambda$ at the outset, the elementary embedding makes this seem global to me. (Although I would not be too surprised if there were a "local" way of phrasing Woodinness.) EDIT: Joel's answer implies that Woodinness actually is a local property, so this answer is of dubious value. In 1976, Magidor published "How large is the first strongly compact cardinal? or A study on identity crises" (http://www.sciencedirect.com/science/article/pii/0003484376900243), in which  among other things  he showed:
However, since every supercompact is a limit of Woodins, this gives that the least strongly compact is above the least Woodin. 

