It is shown that within the language of Set Theory, if membership is assumed to be non-well-founded à la Aczel, then one can state the existence of infinite sets by means of an ∃∃∀∀ 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-Schönfinkel-Ramsey) class of the ∃*∀*- sentences becomes more challenging if no commitment is taken as whether membership is well-founded or not: for this case, we produce an ∃∃∀∀∀-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 ∃∃∀∀.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.
Infinity, in short
OMODEO, Eugenio;POLICRITI, Alberto;TOMESCU, Alexandru Ioan
2012-01-01
Abstract
It is shown that within the language of Set Theory, if membership is assumed to be non-well-founded à la Aczel, then one can state the existence of infinite sets by means of an ∃∃∀∀ 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-Schönfinkel-Ramsey) class of the ∃*∀*- sentences becomes more challenging if no commitment is taken as whether membership is well-founded or not: for this case, we produce an ∃∃∀∀∀-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 ∃∃∀∀.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.File | Dimensione | Formato | |
---|---|---|---|
J Logic Computation-2012-Omodeo-1391-403.pdf
non disponibili
Tipologia:
Versione Editoriale (PDF)
Licenza:
Non pubblico
Dimensione
247.23 kB
Formato
Adobe PDF
|
247.23 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.