There are numerous examples of such statements. Let me organize some of them into several categories.
First, there is the hierarchy of large cardinal axioms that are relatively consistent with V=L. See the list of large cardinals. All of the following statements are provably independent of ZFC+V=L, assuming the consistency of the relevant large cardinal axiom.
There is an inaccessible cardinal.
There is a Mahlo cardinal.
There is a weakly compact cardinal.
There is an indescribable cardinal.
and so on, for all the large cardinals that happen to be relatively consistent with V=L.
These are all independent of ZFC+V=L, assuming the large cardinal is consistent with ZFC, because if we have such a large cardinal in V, then in each of these cases (and many more), the large cardinal retains its large cardinal property in L, so we get consistency with V=L. Conversely, it is consistent with V=L that there are no large cardinals, since we might chop the universe off at the least inaccessible cardinal.
Second, even for those large cardinal properties that are not consistent with V=L, we can still make the consistency statement, which is an arithmetic statement having the same truth value in V as in L.
Con(ZFC)
Con(ZFC+'there is an inaccessible cardinal')
Con(ZFC+'there is a Mahlo cardinal')
Con(ZFC+'there is a measurable cardinal')
Con(ZFC+'there is a supercompact cardinal').
and so on, for any large cardinal property. Con(ZFC+large cardinal property).
These are all independent of ZFC+V=L, assuming the large cardinal is consistent with ZFC, since on the one hand, if W is a model of ZFC+Con(ZFC+phi), then LW is a model of ZFC+V=L+Con(ZFC+phi), as Con(ZFC+phi) is an arithmetic statement. And on the other hand, by the Incompleteness theorem, there must be models of ZFC+¬Con(ZFC+phi), and the L of such a model will have ZFC+V=L+¬Con(ZFC+phi).
Third, there is an interesting trick related to the theorem of Mathias that Dorais mentioned in his answer. For any statement phi, the assertion that there is a countable well-founded model of ZFC+phi is a Sigma12 statement, and hence absolute between V and L. And the existence of a countable well-founded model of a theory is equivalent by the Lowenheim-Skolem theorem to the existence of a well-founded model of the theory. Thus, the truth of each of the following statements is the same in V as in L.
There is a well-founded set model of ZFC. This is equivalent to the assertion: there is an ordinal α such that Lα is a model of ZFC.
There is a well-founded set model of ZFC with ¬CH. (This is also equivalent to the previous statement.)
There is a well-founded set model of ZFC with Martin's Axiom.
and so on. For all the statements known to be forceable, you can ask for a well-founded set model of the theory.
There is a well-founded set model of ZFC with an inaccessible cardinal.
There is a well-founded set model of ZFC with a measurable cardinal.
There is a well-founded set model of ZFC with a supercompact cardinal.
and the same for any large cardinal notion.
These are all independent of ZFC+V=L, since they are independent of ZFC, and their truth is the same in V as in L. I find it quite remarkable that there can be a model of V=L that has a transitive model of ZFC+'there is a supercompact cardinal'. The basic lesson is that the L of a model with enormous large cardinals has very different properties and kinds of objects in it than a model of V=L arising elsewhere. And I believe that this gets to the heart of your question.
Since all these statements are studied very much in set theory, and are very interesting, and are independent of ZFC+V=L, I find them to be positive instances of what was requested.
However, how does this relate to Shelah's view in Dorais's excellent answer? He seems there to dismiss the entire class of consistency strength statements as combinatorics in disguise. What does he mean exactly? Since we set theorists are very interested in these statements, I don't think that he means to dismiss them as silly tricks with the Incompleteness theorem. Perhaps he means something like: to the extent that we believe that a large cardinal property LC is consistent, then we don't really want to consider the theory ZFC+V=L, but rather, the theory ZFC+V=L+Con(LC). That is, we aren't so interested in models having the wrong arithmetic theory, so we insist that Con(LC) if we are comitted to that. And none of the examples I have given exhibit independence from that corresponding theory.
Thanks for clarifying your question. The formulation that
you and Dorais give seems perfectly reasonable. You have a
first order language for category theory, where you can
quantify over objects and morphisms, you can compose
morphisms appropriately and you can express that a given
object is the initial or terminal object of a given
morphism. In this language, one can describe various finite
diagrams, express whether or not they are commutative, and
so on. In particular, one can express that composition is
associative, etc. and describe what it means to be a
category in this way.
The question now becomes: is this theory decidable? In
other words, is there a computable procedure to determine,
given an assertion in this language, whether it holds in
all categories?
The answer is No.
One way to see this is to show even more: one cannot even
decide whether a given statement is true is true in all
categories having only one object. The reason is that group
theory is not a decidable theory. There is no computable
procedure to determine whether a given statement in the
first order language of group theory is true in all groups.
But the one-point categories naturally include all the
groups (and we can define in a single statement in the
category-theoretic language exactly what it takes for the
collection of morphisms on that object to be a group).
Thus, if we could decide category theory, then we could
decide the translations of the group theory questions into
category theory, and we would be able to decide group
theory, which we can't. Contradiction.
The fundamental obstacle to decidability here, as I
mentioned in my previous answer (see edit history), it the
ability to encode arithmetic. The notion of a strongly
undecidable
structure
is key for proving various theories are undecidable. A
strongly undecidable theory is a finitely axiomatizable
theory, such that any theory consistent with it is
undecidable. Robinson proved that there is a strongly
undecidable theory of arithmetic, known as Robinson's Q. A
strongly undecidable structure is a structure modeling a
strongly undecidable theory. These structures are amazing,
for any theory true in a strongly undecidable structure is
undecidable. For example, the standard model of arithmetic,
which satisfies Q, is strongly undecidable. If A is
strongly undecidable and interpreted in B, then it follows
that B is also strongly undecidable. Thus, we can prove
that graph theory is undecidable, that ring theory is
undecidable and that group theory is undecidable, merely by
finding a graph, a ring or a group in which the natural
numbers is interpreted. Tarski found a strongly undecidable
group, namely, the group G of permutations of the integers
Z. It is strongly undecidable because the natural numbers
can be interpreted in this group. Basically, the number n
is represented by translation-by-n. One can identify the
collection of translations, as exactly those that commute
with s = translation-by-1. Then, one can define addition as
composition (i.e. addition of exponents) and the divides
relation is definable by: i divides j iff anything that
commutes with si also commutes with
sj. And so on.
I claim similarly that there is a strongly undecidable
category. This is almost immediate, since every group can
be viewed as the morphisms of a one-object category, and
the group is interpreted as the morphisms of this category.
Thus, the category interprets the strongly undecidable
group, and so the category is also strongly undecidable. In
particular, any theory true in the category is also
undecidable. So category theory itself is undecidable.
Best Answer
"If a set X is smaller in cardinality than another set Y, then X has fewer subsets than Y."
Althought the statement sounds obvious, it is actually independent of ZFC. The statement follows from the Generalized Continuum Hypothesis, but there are models of ZFC having counterexamples, even in relatively concrete cases, where X is the natural numbers and Y is a certain uncountable set of real numbers (but nevertheless the powersets P(X) and P(Y) can be put in bijective correspondence). This situation occurs under Martin's Axiom, when CH fails.