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 in questo prodotto:
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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11390/1038363
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? 2
social impact