This paper considers ∃*∀* prenex sentences of pure first-order predicate calculus with equality. This is the set of formulas which Ramsey's treated in a famous article of 1930. We demonstrate that the satisfiability problem and the problem of existence of arbitrarily large models for these formulas can be reduced to the satisfiability problem for ∃*∀* prenex sentences of Set Theory (in the relators ∈, =). We present two satisfiability-preserving (in a broad sense) translations Φ ↦ (Formula presented.) and Φ ↦ Φσ of ∃*∀* sentences from pure logic to well-founded Set Theory, so that if (Formula presented.) is satisfiable (in the domain of Set Theory) then so is Φ, and if Φσ is satisfiable (again, in the domain of Set Theory) then Φ can be satisfied in arbitrarily large finite structures of pure logic. It turns out that |(Formula presented.)| = (Formula presented.)(|Φ|) and |Φσ| = (Formula presented.)(|Φ|2). Our main result makes use of the fact that ∃*∀* sentences, even though constituting a decidable fragment of Set Theory, offer ways to describe infinite sets. Such a possibility is exploited to glue together infinitely many models of increasing cardinalities of a given ∃*∀* logical formula, within a single pair of infinite sets.

Set-syllogistics meet combinatorics

POLICRITI, Alberto;
2015-01-01

Abstract

This paper considers ∃*∀* prenex sentences of pure first-order predicate calculus with equality. This is the set of formulas which Ramsey's treated in a famous article of 1930. We demonstrate that the satisfiability problem and the problem of existence of arbitrarily large models for these formulas can be reduced to the satisfiability problem for ∃*∀* prenex sentences of Set Theory (in the relators ∈, =). We present two satisfiability-preserving (in a broad sense) translations Φ ↦ (Formula presented.) and Φ ↦ Φσ of ∃*∀* sentences from pure logic to well-founded Set Theory, so that if (Formula presented.) is satisfiable (in the domain of Set Theory) then so is Φ, and if Φσ is satisfiable (again, in the domain of Set Theory) then Φ can be satisfied in arbitrarily large finite structures of pure logic. It turns out that |(Formula presented.)| = (Formula presented.)(|Φ|) and |Φσ| = (Formula presented.)(|Φ|2). Our main result makes use of the fact that ∃*∀* sentences, even though constituting a decidable fragment of Set Theory, offer ways to describe infinite sets. Such a possibility is exploited to glue together infinitely many models of increasing cardinalities of a given ∃*∀* logical formula, within a single pair of infinite sets.
File in questo prodotto:
File Dimensione Formato  
finalICTCS13_OmodeoEtAl.pdf

accesso aperto

Descrizione: versione finale
Tipologia: Documento in Post-print
Licenza: Creative commons
Dimensione 484.07 kB
Formato Adobe PDF
484.07 kB Adobe PDF Visualizza/Apri

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/1119226
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 0
social impact