These sentences are usually of two kinds. The first kind are actually theorems of ZFC asserting the existence of various cardinal numbers and their negations are inconsistent with ZFC. The second kind are the so called "large cardinal axioms" and if A is such a sentence, it cannot be proved (in ZFC) that the consistency of ZFC implies the consistency of ZFC+A. My question is whether any examples of such sentences are known which can be proved (in ZFC) to be undecidable in ZFC-assuming that ZFC is consistent? More precisely, does there exist a formula C(x) in the language of first order ZFC-containing x as its one and only free variable-such that the following three statements are provable in ZFC? (1)If ZFC is consistent, then so is ZFC+"There exists an x such that C(x)" (2)If ZFC is consistent, then so is "ZFC+"There does not exist an x such that C(x)" (3)For all y and z, C(y) and C(z) implies that there exists an injective mapping of y onto z.

These sentences are usually of two kinds. The first kind are actually theorems of ZFC asserting the existence of various cardinal numbers, and their negations are inconsistent with ZFC. The second kind are the so called "large cardinal axioms" and if A is such a sentence, it cannot be proved (in ZFC) that the consistency of ZFC implies the consistency of ZFC+A. My question is whether any examples of such sentences are known which can be proved (in ZFC) to be undecidable in ZFC-assuming that ZFC is consistent? More precisely, does there exist a formula $C(x)$ in the language of first order ZFC  - containing $x$ as its one and only free variable  - such that the following three statements are provable in ZFC? (1) If ZFC is consistent, then so is ZFC+"There exists an $x$ such that $C(x)$" (2) If ZFC is consistent, then so is "ZFC+"There does not exist an $x$ such that $C(x)$" (3) For all $y$ and $z$, $C(y)$ and $C(z)$ implies that there exists an injective mapping of $y$ onto $z$.