The decision problem for a three-sorted fragment of set theory with restricted quantification and finite enumerations

TL;DR

This paper proves the satisfiability problem for a specific three-sorted set theory fragment with restricted quantification and finite enumerations, demonstrating a small model property and expressiveness of set constructs.

Contribution

It introduces a decidable fragment of set theory with restricted quantification and finite enumerations, establishing a small model property and expressive power for set constructs.

Findings

Satisfiability problem is decidable for the fragment.

Any satisfiable formula has a finite model bounded by formula length.

Finite enumerations can significantly shorten formulas involving Cartesian products.

Abstract

We solve the satisfiability problem for a three-sorted fragment of set theory (denoted $3LQST_0^R$), which admits a restricted form of quantification over individual and set variables and the finite enumeration operator $\{\text{-}, \text{-}, \ldots, \text{-}\}$ over individual variables, by showing that it enjoys a small model property, i.e., any satisfiable formula $\psi$ of $3LQST_0^R$ has a finite model whose size depends solely on the length of $\psi$ itself. Several set-theoretic constructs are expressible by $3LQST_0^R$-formulae, such as some variants of the power set operator and the unordered Cartesian product. In particular, concerning the unordered Cartesian product, we show that when finite enumerations are used to represent the construct, the resulting formula is exponentially shorter than the one that can be constructed without resorting to such terms.