Russells_Paradox
Disprovedantinomiesnaive-set-theoryproofwikiretryrussell-s-paradoxsubsets
There is no predicate that holds for exactly those elements for which it does not hold (Russell's paradox).
Formal statement
theorem Russells_Paradox {α : Type _} (S : α → Prop) : ¬ (∀ x : α, S x ↔ ¬ S x) := by sorry