### Lesniewski and Frege's way out

Recall that Frege, when faced with Russell's paradox, replaced the left-to-right direction of his Basic Law V:
{x:F(x)}={x:G(x)} → ∀x[F(x)↔G(x)]
with something like:
{x:F(x)}={x:F(x)}→∀y[[y≠{x:F(x)}]→ F(y)↔G(y)]
This move came to be referred to as Frege's way out (I think this name dates back to Quine's 1955 Mind paper, but that's just a guess).

Right now, I'm reading Giaquinto's The Search for Certainty. It's a very clear and accessible account of main debates surrounding foundations of mathematics pretty much from Dedekind and Cantor to GĂ¶del. I really like the book, it's fun to read, the account is clear and succinct, and the author provides well-defended critical assessment of the views he discusses.

One remark. In footnote 22 (to ch. 3, part 2) Giaquinto's remarks that Lesniewski has already shown that Frege's way out still leads to contradiction.

This isn't exactly right. Strictly speaking, what Lesniewski has shown is rather that Frege's way out leads to contradiction with three additional assumptions (well, after translation from Lesniewski's language):
1. ∀F[∃xF(x)→∃y(y={z:F(z)})]
2. ∀F∀x,y[x={z:F(z)} & y={u:F(u)} → x=y]
3. ∃x,y,z[x≠ y & x ≠ z & y≠z]
The first says that if something is F, then the class of F's exists. The second says that the class operator is a function (this is especially non-trivial in Lesniewski's systems), so that when you have a concept F, 'the extension of F' will name at most one object. (In a sense, assumption 2 corresponds to an instance of the right-to-left direction of Basic Law V). The third says that there are at least three distinct objects.

For an excruciatingly boring but a fairly detailed account of these (and related) things, see this paper. If you want to see a streamlined version of Lesniewski's proof on the blog, let me know in a comment and I might come up with a short version.