Naively addressing Russell's paradox

What you are looking for is actually very elegant: 3-valued logic instead of classical logic. You are then free to construct a type given any defining formula, but membership may not be boolean. Call the types with boolean membership "classes". You can further stipulate that every type constructed using only classes in its defining formula is itself a class. (Here we consider $x$ as used if it appears in the form "$\in x$".) Then $U \overset{def}= \{ x : x=x \}$ is a class, of which every object is a member, including $U$ itself. $ \def\nn{\mathbb{N}} \def\qq{\mathbb{Q}} \def\rr{\mathbb{R}} $

Russell's paradox disappears, because $R \overset{def}= \{ x : x \notin x \}$ is not a class, and so $R \in R$ is not boolean and there will be no contradiction. From a computability perspective $R$ is like a recursive program that is not total, and "$R \in R$" does not halt. Interpreting objects as strings and types as programs also gives an obvious model for this system, where $U$ is simply the collection of all finite strings, clearly decidable by a program.

The next natural question is what other classes there should be. One obvious one is that $\nn$ ought to be a class, consistent with any natural encoding of naturals as strings. But since we want classes to be closed under quantification over classes, we would need to expand our model to have programs that use any (constant) finite Turing jump. If you have PA$^-$ for $\nn$, then every arithmetical set is a class. And hence if you also have the full induction schema on $\nn$ (for all sentences over the system) then you will be able to interpret ACA and hence recover nearly all real-world mathematics.

If you are a set theorist, you might want the powertype of $\nn$ to be a class as well, but in some sense that is felt by many logicians to be unsafe from a predicative perspective; you will find them saying that $Z_2$ (full second-order arithmetic) is impredicative. Indeed, there are three ways we can justify this viewpoint in this system:

1. Let $S \overset{def}= \{ x : \forall y \in x\ ( y \in \nn ) \}$, but due to the "$\in x$" we cannot conclude that it is a class. And for good reason! We can construct $T \overset{def}= \{ x : \{ y : y \in \nn \lor x \in x \} \in S \}$. If $S$ is a class, then $T$ is also a class, and hence $V \overset{def}= \{ y : y \in \nn \lor T \in T \}$ is also a class. But if $T \notin T$, then $V \in S$ by definition of $V,S$, and hence $T \in T$ by definition of $T$. And if $T \in T$, then everything is in $V$ by definition of $V$, yet $V \in S$ and hence everything is in $\nn$. Presumably not what you want!

2. Even if you want everything to be a natural number, we can use a modified variant of (1) that shows that the powertype of the positive naturals, namely $S' \overset{def}= \{ x : \forall y \in x\ ( y \in \nn \land y \ne 0 ) \}$, cannot be a class, where in the ensuing argument $0$ would be the witness that not everything is in $\nn_{\ne 0}$.

3. Let $Class \overset{def}= \{ x : \forall y\ ( y \in x \lor y \notin x ) \}$, namely the type of all classes. Then we have another variant of (1): Let $S'' \overset{def}= \{ x : x \in Class \land \forall y \in x\ ( y \in \nn ) \}$. Here the "$\in Class$" is the only part that stops us from concluding that $S''$ is a class, and it had better do so because the same argument as before shows that it cannot be.

Although the above implies that we can no longer treat the powertype of the naturals as a class like in classical set theories, it does not really affect much of common mathematics. We still can deduce statements involving the subclasses of naturals, namely $S''$, as long as it is used as a type, just as in ordinary classical mathematics, because typically you never use $S''$ for anything else. What differs is that if we construct a type of objects whose defining formula uses "$\in S''$", then that type may not be a class and so cannot be used to define a subclass of natural numbers.

For example, $\qq$ can be easily constructed, and if we have inbuilt or definable pairing functions, we can then construct the type of Cauchy sequences from $\qq$ and from that the type of real numbers $\rr$. It does not matter that $\rr$ is not a class, since every statement of real analysis that merely involves quantifying over $\nn$ and $\rr$ and function types over them can still be proven.

Notice that there is absolutely no restriction on type specification, but not all types are classes. But there is a universal class, which is impossible in classical set theories. Furthermore, the above system is consistent with having a class $E$ whose only member is itself, in much the same way that there is a program that halts on every input and outputs "true" iff the input is its own source code. This is a nice puzzle in itself!

In summary your idea of ambiguity can be cleanly captured by 3-valued logic, and your idea of unambiguous sets is captured by classes.

Typically the relation "$\notin$" is defined by $x \notin y \iff \neg (x \in y)$, so logic alone tells us that "we cannot allow both statements [$R\in R$ and $R \notin R$] to be false." Moreover, redefining "$\notin$" to mean something else would not affect the paradox: we could just say $R = \{x : \neg(x \in x)\}$ instead of $R = \{x : x \notin x\}$.

EDIT: I think I may have missed the main point of the question, which is a proposed weakening of unrestricted comprehension that only allows us to define sets $\{x : P(x)\}$ in the case that "membership is unambiguous." As pointed out in a comment by columbus8myhw, this is problematic because it's not clear how unambiguity can be phrased as a syntactical property of $P$ (or how it can be made precise at all, I might add.)

In particular, it's not clear how we are supposed to know a priori that there is anything "ambiguous" about "$\neg (x \in x)$". There may be lots of ways to weaken the unrestricted comprehension schema in order to avoid Russell's contradiction, but from what is written in the question it's hard to tell exactly which weakening is being proposed.

Russell's paradox is that the definition $R := \{x \mid x \not\in x\}$ implies that $R \in R$ and $R \not\in R$ are false. According to the above paragraph, Russell's paradox simply implies that $R$ is not a set. In other words, the above definition only allows statements of the form $\{x \mid P(x)\}$ to be sets if membership is unambiguous for every $x$.

Actually, Russell's Paradox is that, in so-called naive set theory, you could both prove and disprove that $$\exists R:\forall x:[x\in R\iff x\notin x]$$

It could be proven by applying the axiom of unrestricted comprehension that was a feature of naive set theory. Disallowing unrestricted comprehension made it impossible to derive the above theorem.

The disproof was still possible since it was based only on applications of the rules and axioms of first-order logic.