# Can we extend a version of MK with that coding function?

Lets weaken the limitation of size axiom of MK to that of sets, i.e. every class that is subnumerous to a set is a set, now to that version of $$MK$$ lets add to the language of it a primitive unary coding function $$Cd$$, and restrict class comprehension axiom of $$MK$$ to pure class theoretic formulas (i.e. formulas not using $$Cd$$), and add an axiom that all codes are sets, i.e. $$[y=Cd(x) \to y \in V]$$, where $$V$$ is the class of all sets. Also axiomatize that the coding function is bijective. Now to the resulting theory can we add the following schemata?

Class coding schema: if $$\varphi(z)$$ is a formula in $$L(=,\in)$$, in which $$x$$ is not free, then: $$\exists x \forall y (y \in x \leftrightarrow \exists z (\varphi(z) \wedge y=Cd(z)))$$

Set coding scheme: if $$\varphi^V(z)$$ is a formula in which all of its quantifiers are bounded in $$V$$, then for all set closures we have:

$$\exists x \forall y (y \in x \leftrightarrow \exists z \in V (\varphi^V(z) \wedge y=Cd(z)))$$

In English: The class coding scheme states that we can construct any class of codes of classes as long as the latter ones are predicated in pure class language. While the set coding schema states that we can construct any class of codes of sets predicated by formulas restricted to sets but allowed to use the coding function.

From that we can for example define Cardinality by a modification of Scott's trick, as Cardinality of any class $$x$$ is the class of all codes of classes equinumerous to $$x$$ of the lowest possible rank. Also I think we can code an embedding from $$V$$ to $$V$$ by using the Set coding scheme.

• Presumably you want to include additional axioms - what if $Cd(y)=\emptyset$ for every $y$? At the very least you want $Cd$ to be injective I think ... – Noah Schweber Jan 6 at 11:00
• Yes, that's perfectly correct, actually I need it to bijective. Thanks – Zuhair Jan 6 at 11:01