# Why does the Second-Order Axiom schema of Comprehension not lead to Russell's Paradox for ZFC2?

Let ZFC2 be the Second-Order formalisation of ZFC.

The Second-Order Axiom schema of Comprehension (part of the deductive system for SOL) says that for every formula (of SOL) there is a relation with the same extension (shapiro 1991).

If we formalise ZFC2, then the domain is all sets and the second-order quantifiers range over all the subsets of the domain. But then, what stops Russell's Paradox from arising?

I know it doesn't because ZFC2 is equivalent to Morse-Kelley set theory.

In Second-order Logic, the comprehension schema (considering for simplicity only unary predicate variables) is:

∃X∀x [ ϕ(x) ↔ X(x) ],

where x is an individual variable, X is a 1-ary predicate variable and X may not occur free in ϕ.

What prevents form generating Russell's Paradox ?

Two facts:

(i) we cannot substitute X for x.

A s-o language for sets must use individual variables x for sets and unary predicate variables for classes. So, x ∈ A must be formalized as A(x) and thus, using it as ϕ(x), what we get is:

∃X∀x [ ~A(x) ↔ X(x) ].

(ii) the proviso that X may not be free in ϕ prevents from using ~X(x) to get:

∃X∀x [ ~X(x) ↔ X(x) ].