Stratified comprehension burns down to acyclic comprehension, however not all cyclic formulas are pathological, indeed the standard set theory ZF do heavily use cyclic formulation. This method allows some cyclic formulas to define sets but of course, imposes the restriction that under certain specifications (outlined below) no Looping is acceptable. So it identifies the existence of LOops on specifically defined graphs on formulas to be the culprit.
A formula phi is said to be a NON-LOOP formula if and only if:
Predicate restriction: it only uses E as non-logical predicate symbol
Typo-graphical restriction: for every bound variable x in phi, all occurrences of x must be bound by the same quantifier.
Loop checking: we can assign a function from variables in phi to the naturals such that for every atomic subformula x E y of phi, x is assigned a type lower than the type of y.
Upward typing: we define assignment of naturals to variables in phi such that all bottom variables (variables only occurring on the left side of the membership symbol "E" in phi) will be assigned type 1, then we type the rest of variables in phi upwardly such that for every atomic formula y E x, x will be assigned one type higher than that of y, so each variable can be assigned a set of types, now once the process is completed, the upward type of the variable is the highest one in the set of types assigned to it.
Downward typing: we keep all upward assignments given to the top variables in phi (i.e. variables only occurring on the right of the membership symbol "E" in phi), and we delete all upward assignments to other variables in phi, and we start typing them downwardly such that for each atomic formula x E y, x will be assigned one type lower than that of y, so each variable will be assigned a set of types, now once the process is completed, the downward type of the variable is the highest one in the set of types assigned to it.
Impredicativity check: we add to phi a formula z E k if k and z are bound variables in phi and k lies within the quantification scope of z, i.e., we have z(...k(, and if at the same time k is assigned a higher or equal type to that of z at step 5, to result in formula phi+
Loop checking: we can assign a function from variables in phi+ to the naturals such that for every atomic subformula x E y of phi+, x is assigned a type lower than the type of y.
Axiom scheme of LOop Comprehension: if phi(y) is a non-loop formula, in which x doesn't occur free, then (Exists x for all y (y E x <-> phi(y))) is an axiom.
This theory does interpret NF, and I think it also proves the consistency of Zermelo, and I'd conjecture that it would prove the consistency of ZF as well.
at 29/10/2017
Now I figured out that this won't work, I can simply reproduce Russell's paradox in a rather straightforward manner! The formula Exist z (for all y (x E y -> z E y) ^ ~ z E x) is a non-loop formula and still, it easily defined the Russell's set
It would interesting to see if the whole way is salvageable?