The axiom scheme of acyclic comprehension

A "new" criterion for set existence is presented, namely, that a set {x | φ} should exist if the multigraph whose nodes are variables in ' and whose edges are occurrences of atomic formulas in ' is acyclic. Formulas with acyclic graphs are stratified in the sense of New Foundations, so consistency of the set theory with weak extensionality and acyclic comprehension follows from the consistency of Jensen's system NFU. It is much less obvious, but turns out to be the case, that this theory is equivalent to NFU: it appears at first blush that it ought to be weaker. This paper verifies that acyclic comprehension and stratified comprehension are equivalent by verifying that each axiom in a finite axiomatization of stratified comprehension follows from acyclic comprehension.