Can ZFC commit cardinality errors?

Question

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.

Answer 1

We assume |X| is the least von Neuman ordinal for which there is a bijection from it to X. Then ZFC cannot "commit cardinality error of the second kind". This is true because your axiom scheme and rule of inference hold in ZFC when c(X) is |X|.

In order to verify the rule of inference holds when c(X) is |X|, suppose 𝜓(𝑋)∧𝜑(𝑌) and |X|=|Y|. Then there is a bijection f between X and Y. Let 𝜙(𝑥,𝑦,z) be the formula (xy)∈z. Then (∀𝑥∈𝑋∃!𝑦∈𝑌(𝜙(𝑥,𝑦,f))∧∀𝑦∈𝑌∃!𝑥∈𝑋(𝜙(𝑥,𝑦,f).

Please note that the statement "Now NFU is an example of a set theory that commit cardinality error of the first kind, but this cannot occur in ZFC." is misleading because usually |X| has a different meaning in ZF then in NF.

I deleted my last comment because it was not correct, and am adding the answers to the modified(parameters not allowed) questions. If ZF is consistent, then the answer to the first modified questions is no. If ZF is consistent so is ZF+V=L. The modified axioms and rules of inference hold in ZF+V=L when c(X) is interpreted as |X|. Let < be a definable well ordering of the universe. In order to verify the rule of inference holds when c(X) is |X|, suppose 𝜓(𝑋)∧𝜑(𝑌) and |X|=|Y|. Let b be the least cardinal such that there exist s and t for which 𝜓(s)∧𝜑(t) and |s|=|t|=b. Let x be <-least such that 𝜓(x) and |x|=b. Let y be <-least such that 𝜑(y) and |y|=b. Let f be the <-least bijection from x to y. Let 𝜙(s,t) be a formula which holds when and only when f(s)=t. Then (∀s∈x∃!t∈y(𝜙(s,t))∧∀t∈y∃!s∈x(𝜙(s,t). If ZF is consistent then the answer to the second modified question is yes because "ZFC doesn't commit cardinality error of the second kind" implies Con(ZF).

Answer 2

This principle as written isn't appropriate for the class of theories including NF and NFU. If the formula $\phi$ is restricted to be stratified and have $x$ and $y$ of the same relative type then the principle is true in NF and so in any of its fragments (this is the real answer).

In NF, the universe is a set, the set of all singletons is a set, and there can be no bijection between them. Suppose there were such a bijection f from singletons onto sets. Then we could define the set $R = \{x : \lnot (x \,E\, f(\{x\}))\}$ (this definition would be stratified). Now consider $f^{-1}(R) = \{r\}$, $r \,E\, R \iff \lnot \ r \,E \,R$ follows.

There are fragments of NF in which this argument does not work: these inevitably have seriously impaired comprehension principles and are very weak. I believe that in versions of NF with predicativity restrictions on comprehension, one can arrange for all infinite sets to be the same size. But mathematically these systems are quite weak, and the principle Zuhair suggests becomes true in a trivial sense.