Add a primitive a one place function symbol $c$ to represent "True cardinality" of a set, to the first order language of set theory.

Add the following axiom schema:

**1. Cardinal Equality:** If $\phi(x,y)$ is a formula in which *both and only* $x,y$ occur free, and only occur free, then all closures of: 

$\forall X,Y: \\\forall x \in X \exists! y \in Y (\phi(x,y)) \land  \\\forall y \in Y \exists! x \in X (\phi(x,y)) \\ \to c(X)=c(Y)$ 

are axioms.

Add the following $\omega$-rule of inference:

**2. Cardinal Inequality:** If $\psi(X); \varphi(Y)$, are formulas in which $X,Y$ occur free and only free respectively, then:

From: $\big{[}$if $\phi(x,y)$ is a formula in which *both and only* $x,y$ occur free, and they only occur free, then all closures of the following formula are true:

 $\forall X,Y (\psi(X) \land \varphi(Y) \to \\\neg [\forall x \in X \exists! y \in Y (\phi(x,y)) \land  \\\forall y \in Y \exists! x \in X (\phi(x,y))]) \big{]}$

______________________we Infer 

All closures of $\forall X,Y (\psi(X) \land \varphi(Y) \to c(X)\neq c(Y) )$ are true.


Now if a set theory T extended with the above, proves that:

$\exists X,Y: |X|\neq|Y| \land c(X)=c(Y)$

Then its guilty of committing cardinaity error of the first kind.

If it proves that:

$\exists X,Y: |X| = |Y| \land c(X) \neq c(Y)$

Then its guilty of committing cardinality error of the second kind.

Now NFU is an example of a set theory that commit cardinality error of the first kind, but this cannot occur in ZFC.

> Can ZFC commit cardinality error of the second kind?

Based on comments with Monroe Eskew. The following question presents itself.

>Is there a natural statement that the theory "ZFC + ZFC doesn't commit cardinality error of the second kind" can settle, that ZFC + V=L cannot? 

**NOTE:** The axiom schema and the $\omega$-inference rule had been edited, the prior version didn't require $x,y$ to be the sole free variables in $\phi(x,y)$ and that older version was answered by Greg Kirmayer towards ZFC proving that it cannot commit error of second kind, but it did this via a parameter. The more restrictive version present above is meant to enforce a restrictive principle on ZFC, and the second question is about such a restriction. 

**After note** if we are testing whether a theory T is committing a cardinality error, then only primitives of theory T are allowed in the cardinal equality schema and the cardinal inequality inference rule, i.e. $c$ cannot be used.