Infinity, in short

• Published in: Journal of logic and computation 2012-12, Vol.22 (6), p.1391-1403
• Main Authors: Omodeo, E. G., Policriti, A., Tomescu, A. I.
• Format: Article
• Language: English
• Subjects: Computation; Formulations; Infinity; Reduction; Sentences; Set theory; Specifications; Symbols
• ISSN: 0955-792X; 1465-363X
• DOI: 10.1093/logcom/exr020

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 [exist][exist][forall][forall] 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 [exist]*[forall]*-sentences becomes more challenging if no commitment is taken as whether membership is well-founded or not: for this case, we produce an [exist][exist][forall][forall][forall] -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 [exist][exist][forall][forall].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.