I can’t say anything about this specific construction, but there is a related issue in Turing machines. The issue was whether you could determine a useful subset S of the set of all Turing machines, such that the halting problem is solveable for all machines in S, and S was general enough to contain useful examples.
If I remember correctly, the answer was that you couldn’t. This feels a lot like that—I’d bet that the only way of being sure that we can avoid Russel’s paradox is to restrict predicates to such a narrow category that we can’t do much anything useful with them.
I can’t say anything about this specific construction, but there is a related issue in Turing machines. The issue was whether you could determine a useful subset S of the set of all Turing machines, such that the halting problem is solveable for all machines in S, and S was general enough to contain useful examples.
If I remember correctly, the answer was that you couldn’t. This feels a lot like that—I’d bet that the only way of being sure that we can avoid Russel’s paradox is to restrict predicates to such a narrow category that we can’t do much anything useful with them.