Editing Russell's paradox (section)

== Formal presentation ==
The term "[[naive set theory]]" is used in various ways.  In one usage, naive set theory is a formal theory, that is formulated in a [[predicate logic|first-order language]] with a binary non-logical [[Predicate (mathematical logic)|predicate]] <math>\in</math>, and that includes the [[axiom of extensionality]]:
: <math>\forall x \, \forall y \, ( \forall z \, (z \in x \iff z \in y) \implies x = y)</math>
and the axiom schema of [[unrestricted comprehension]]:
: <math> \exists y \forall x (x \in y \iff \varphi(x))</math>
for any predicate <math>\varphi</math> with {{mvar|x}} as a free variable inside <math>\varphi</math>. Substitute <math>x \notin x</math> for <math>\varphi(x)</math> to get
: <math> \exists y \forall x (x \in y \iff x \notin x)</math>

Then by [[existential instantiation]] (reusing the symbol <math>y</math>) and [[universal instantiation]] we have
: <math>y \in y \iff y \notin y ,</math>
a contradiction.  Therefore, this naive set theory is [[Consistency|inconsistent]].<ref>{{cite encyclopedia |title= Russell's Paradox|encyclopedia=The Stanford Encyclopedia of Philosophy |year= 2014 |editor-last= Zalta|editor-first= Edward N.|url=http://plato.stanford.edu/archives/win2014/entries/russell-paradox/|last1= Irvine|first1=Andrew David|last2= Deutsch|first2= Harry }}
</ref>