Thinking on the theory NBG (of von Neumann–Bernays–Gödel) I arrived at the conclusion that it is contradictory using an argument resembling Russell's Paradox. I am sure that I made a mistake in my arguments (because NBG cannot be contradictory, as all mathematicians believe), but I can not find the exact place where the error happened.
The theory NBG is finitely axiomatizable theory whose undefined notions are "class" and "element". A class is called a set if it is an element of some other class. The axioms of NBG imply the existence of the universal class $\mathbf V$ containing all sets as elements. Axioms of NBG allow to make the following six basic operations over classes $X$, $Y$:
The difference: $X\setminus Y=\{z:z\in X\wedge z\notin Y\}$;
The Cartesian product: $X\times Y=\{\langle x,y\rangle:x\in X\wedge y\in Y\}$;
The transposition: $X^{-1}=\{\langle y,x\rangle:\langle x,y\rangle\in X\}$;
The cyclic permutation: $X^\circlearrowright=\{\langle\langle z,x\rangle,y\rangle:\langle\langle x,y\rangle,z\rangle\in X\}$;
The domain: $\DeclareMathOperator\dom{dom}\dom[X]=\{x:\exists y\;\langle x,y\rangle\in X\}$.
The membership: $X_\in=\{\langle x,y\rangle\in X:x\in y\}$.
A class $X$ is called constructible if it can be constructed from the universal class $\mathbf V$ applying finitely many basic operations over classes. For example, the empty set is constructible because $\emptyset=\mathbf V\setminus\mathbf V$. Gödel's Class Existence Theorem implies that a class is constructible if it can be described by a formula with a unique parameter $\mathbf V$ and all quantifiers running over elements of $\mathbf V$. It is clear that there are only countably many constructible classes.
All possible compositions of basic operations can be effectively enumerated by the set $T=\bigcup_{n\in\omega}7^{2^{<n}}$ of 7-labeled full binary trees of finite height.
The idea of this enumeration is as follows. First, enumerate the basic operations over classes $X$, $Y$:
\begin{align*} & G_0(X,Y):=X, \\ & G_1(X,Y):=X\setminus Y, \\ & G_2(X,Y)=X\times Y, \\ & G_3(X,Y):=X^{-1}, \\ & G_4(X,Y)=X^\circlearrowright \\ & G_5(X,Y):=\dom[X], \\ & G_6(X,Y)=X_\in. \end{align*}
Let $2^{<\omega}=\bigcup_{n\in\omega}2^n$ be the full binary tree and for every $n\in\omega$, let $2^{<n}=\bigcup_{k\in n}2^k$ be the full binary tree of height $n$. For every $k\in\{0,1\}$, consider the function $\vec k:2^{<\omega}\to 2^{<\omega}$, $\vec k:f\mapsto \{\langle 0,k\rangle:\langle i+1,v\rangle:\langle i,v\rangle\in f\}$ and observe that $\vec k[2^n]\subseteq 2^{n+1}$.
For every $n\in\omega$, function $\lambda:2^{<n}\to 7=\{0,1,2,\dotsc,6\}$, and class $X$, consider the class $G_\lambda(X)$ defined by the recursive formula $G_\lambda(X)=X$ if $n=0$ and $G_\lambda(X)=G_{\lambda(0)}(G_{\lambda\circ \vec 0}(X),G_{\lambda\circ \vec 1}(X))$ if $n>0$. So, $G_\lambda$ represents a composition of the basic operations taken in the order suggested by the labels at the vertices of the binary tree $2^{<n}$.
A class $X$ is constructible if and only if $X=G_\lambda(\mathbf V)$ for some $n\in\omega^\star$ and $\lambda\in 7^{2^{<n}}$. Here $\omega^\star$ is the set of "standard" numbers in the model of NBG. So, the constructibility of classes is an external notion to the model of NBG. Here we assume that NBG is not contradictory and fix some model of NBG. This model contains an element $\omega$ whose elements are natural numbers in the model. Among those natural numbers, there are standard natural numbers, which are successors of the empty set (from the viewpoint of the universe in which the model of NBG lives).
Let $T=\bigcup_{n\in\omega}7^{2^{<n}}$ be the set of all 7-labeled binary trees of finite height. This set is a countable constructible subset of the model.
Claim. There exists a constructible class $C\subseteq T\times\mathbf V$ such that for every standard number $n\in\omega^\star$ and every 7-labeled tree $\lambda\in 7^{2^{<n}}$, the class $C_\lambda=\{x\in \mathbf V:\langle\lambda,x\rangle\in C\}$ coincides with the class $G_\lambda(\mathbf V)$.
Assume for a moment that the Claim is proved. The constructibility of the class $C$ implies the constructibility of the class $\Lambda=\{\lambda\in T:\langle\lambda,\lambda\rangle\notin C\}$. Then there exists a standard number $n\in\omega^\star\subseteq\omega$ and a 7-labeled tree $\lambda\in 7^{2^{<n}}$ such that $\Lambda=C_\lambda:=\{x\in\mathbf V:\langle\lambda,x\rangle\in C\}$. Now we have a paradox of Russell's type:
if $\lambda\in\Lambda$, then $\lambda\in C_\lambda$ and hence $\langle\lambda,\lambda\rangle\in C$ and $\lambda\notin\Lambda$;
if $\lambda\notin\Lambda$, then $\langle\lambda,\lambda\rangle\in C$ and hence $\lambda\in C_\lambda=\Lambda$.
In both cases, we obtain a contradiction.
Proof of Claim. Let $\mathbf{On}$ be the class of ordinals and $(V_\alpha)_{\alpha\in\mathbf{On}}$ be the von Neumann hierarchy, which can be identified with the class $\bigcup_{\alpha\in\mathbf{On}}\{\alpha\}\times V_\alpha$. It can be shown that both these classes are constructible (because they can be defined by formulas in which quantifiers run over elements of the universal class $\mathbf V$). It can be shown that for every standard number $n\in\omega^\star\subseteq\omega$, every 7-labeled tree $\lambda\in 7^{2^{<n}}$ and every ordinal $\alpha$ there exists an ordinal $\beta$ such that $V_\alpha\cap G_\lambda(\mathbf V)=V_\alpha\cap G_\lambda(V_\gamma)$ for all ordinals $\gamma\ge\beta$.
Applying the Theorem of Recursion, for every ordinals $\alpha,\beta$ one can construct a class $C_{\alpha,\beta}\subseteq T\times\mathbf V$ such that for every standard number $n\in\omega^\star\subseteq\omega$ and 7-labeled tree $\lambda\in 7^{2^{<n}}$ we have $\{x\in \mathbf V:\langle \lambda,x\rangle\in C_{\alpha,\beta}\}=V_\alpha\cap C_\lambda(V_\beta)\}$. Moreover, the recursive definition of the indexed sequence $(C_{\alpha,\beta})_{\alpha,\beta\in\mathbf{On}}$ shows that it is constructible as a subclass of $\mathbf{On}\times\mathbf{On}\times T\times\mathbf V$ (because it is defined by a formula whose quantifiers run over elements of the universal set). For every ordinal $\alpha$ consider the class $$C_\alpha=\{\langle\lambda,x\rangle\in T\times\mathbf V:\exists \beta\in\mathbf{On}\;\forall \gamma\in \mathbf{On}\; (\beta\le \gamma\to \langle \lambda,x\rangle \in C_{\alpha,\gamma})\}.$$ The constructibility of the family $(C_{\alpha,\beta})_{\alpha,\beta\in \mathbf{On}}$ implies the constructibility of the set indexed family $(C_\alpha)_{\alpha\in\mathbf {On}}$ (identified with the subclass $\bigcup_{\alpha\in\mathbf{On}}\{\alpha\}\times C_\alpha$ of the class $\mathbf{On}\times (T\times\mathbf V)$. The constructibility of the indexed family $(C_\alpha)_{\alpha\in\mathbf{On}}$ implies the constructibility of the class $$C=\{\langle \lambda,x\rangle\in T\times\mathbf V:\exists \alpha\in\mathbf{On}\;\langle\lambda,x\rangle\in C_\alpha\},$$ which has the property, required in the Claim. $\square$
So
Question. In which place does this argument proving the inconsistency of NBG contain a gap?
