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.