Set-syllogistics meet combinatorics. (11th May 2015)

• Record Type: Journal Article
• Authors: OMODEO, EUGENIO G.; POLICRITI, ALBERTO; TOMESCU, ALEXANDRU I.
• Is Part Of: Mathematical structures in computer science. Volume 27:Number 2(2017)
• Page Start: 296
• Page End: 310
• Publication Date: 2015-05-11
• Subjects: Computer science -- Mathematics -- Periodicals; 004.015105
• DOI: 10.1017/S0960129515000122
• Languages: English
• ISSNs: 0960-1295

Abstract

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 Φ ↦ $\dot{\Phi}$ and Φ ↦ Φ σ of ∃*∀* sentences from pure logic to well-founded Set Theory, so that if $\dot{\Phi}$ 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 | $\dot{\Phi}$ | = $\mathcal{O}$ (|Φ|) and |Φ σ | = $\mathcal{O}$ (|Φ| 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.