Set-syllogistics meet combinatorics. (11th May 2015) - OMODEO, EUGENIO G.; POLICRITI, ALBERTO; TOMESCU, ALEXANDRU I.
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{Φ}$ and Φ ↦ Φ σ of ∃*∀* sentences from pure logic to well-founded Set Theory, so that if $\dot{Φ}$ 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{Φ}$ | = $\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.