Russell's paradox and the Y combinator

I studied both (λ-calculus and Set Theory) academically and the description IS disjointed and difficult to read. I get what OP is trying to say because I already understand these concepts.<p>But even though the isomorphism between the Y combinator and Russell&#x27;s paradox is elegant, the paradox is actually very deep (much deeper than the idea of a fixed point) -- that&#x27;s why it took someone until the early 20th century to formalize it. For an awesome (and mind-blowing) explanation of the paradox, see Halmos&#x27; Naive Set Theory (botom of page 6): <a href="http:&#x2F;&#x2F;sistemas.fciencias.unam.mx&#x2F;~lokylog&#x2F;images&#x2F;stories&#x2F;Alexandria&#x2F;Logica%20y%20Conjuntos&#x2F;Paul%20R.Halmos%20-%20Naive%20Set%20Theory.pdf" rel="nofollow">http:&#x2F;&#x2F;sistemas.fciencias.unam.mx&#x2F;~lokylog&#x2F;images&#x2F;stories&#x2F;Al...</a>

I found this description disjointed and difficult to read.

I&#x27;ve read that languages for mathematical reasoning (such as Coq) are not Turing-complete to avoid issues like this. We can tolerate the possibility of infinite loops when we actually execute a program and see that it returns an answer, but apparently programs used as proofs aren&#x27;t actually run, so type-checking needs to eliminate this sort of paradox.

Good stuff. A bit of googling got me to Curry&#x27;s Paradox [0] which is really just a different statement of this. Self-reference breaks things.<p>[0] <a href="http:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Curry%27s_paradox#Existence_problem" rel="nofollow">http:&#x2F;&#x2F;en.wikipedia.org&#x2F;wiki&#x2F;Curry%27s_paradox#Existence_pro...</a>

Russell is spelt wrong