The Satisfiability Problem for Boolean Set Theory with a Choice Correspondence

Electronic Proceedings in Theoretical Computer Science ◽

10.4204/eptcs.256.5 ◽

2017 ◽

Vol 256 ◽

pp. 61-75 ◽

Cited By ~ 1

Author(s):

Domenico Cantone ◽

Alfio Giarlotta ◽

Stephen Watson

Keyword(s):

Set Theory ◽

Satisfiability Problem ◽

Choice Correspondence

Download Full-text

Set-syllogistics meet combinatorics

Mathematical Structures in Computer Science ◽

10.1017/s0960129515000122 ◽

2015 ◽

Vol 27 (2) ◽

pp. 296-310 ◽

Cited By ~ 8

Author(s):

EUGENIO G. OMODEO ◽

ALBERTO POLICRITI ◽

ALEXANDRU I. TOMESCU

Keyword(s):

Set Theory ◽

Satisfiability Problem ◽

Single Pair ◽

Logical Formula ◽

First Order ◽

Finite Structures ◽

Pure Logic ◽

Decidable Fragment ◽

Infinite Sets ◽

Order Predicate Calculus

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.

Download Full-text