Infinity, in short
It is shown that within the language of Set Theory, if membership is assumed to be non-well-founded a la Aczel, then one can state the existence of infinite sets by means of an there exists there exists for all for all prenex sentence. Somewhat surprisingly, this statement of infinity is essentially the one which was proposed in 1988 for well-founded sets, and it is satisfied exclusively by well-founded sets. Stating infinity inside the BSR (Bernays Schonfinkel Ramsey) class of the there exists*for all*-sentences becomes more challenging if no commitment is taken as whether membership is well-founded or not: for this case, we produce an there exists there exists for all for all for all-sentence, thus lowering the complexity of the quantificational prefix with respect to earlier prenex formulations of infinity. We also show that no prenex specification of infinity can have a prefix simpler than there exists there exists for all for all. The problem of determining whether a BSR-sentence involving an uninterpreted predicate symbol and = can be satisfied over a large domain is then reduced to the satisfiability problem for the set theoretic class BSR subject to the ill-foundedness assumption. Envisaged enhancements of this reduction, cleverly exploiting the expressive power of the set theoretic BSR-class, add to the motivation for tackling the satisfaction problem for this class, which appears to be anything but unchallenging.
satisfiability computable set theory bernays-schonfinkel-ramsey class infinity axiom non-well-founded sets decision algorithms mathematics subject classification (2000) 03e30 03e70