On the satisfiability problem for a 3-level quantified syllogistic

TL;DR

This paper investigates the satisfiability problem for a specific three-sorted set-theoretic language, proving small model properties and NP-completeness for certain fragments, and formalizing modal logic S5 within one fragment.

Contribution

It introduces the TLQSR language with a small model property and NP-complete fragments, and formalizes modal logic S5 in a restricted sublanguage.

Findings

TLQSR has a small model property for satisfiable formulas.

Fragments (TLQSR)^h are NP-complete for h ≥ 2.

Modal logic S5 can be formalized in (TLQSR)^3.

Abstract

We show that a collection of three-sorted set-theoretic formulae, denoted TLQSR and which admits a restricted form of quantification over individual and set variables, has a solvable satisfiability problem by proving that it enjoys a small model property, i.e., any satisfiable TLQSR-formula psi has a finite model whose size depends solely on the size of psi itself. We also introduce the sublanguages (TLQSR)^h of TLQSR, whose formulae are characterized by having quantifier prefixes of length bounded by h \geq 2 and some other syntactic constraints, and we prove that each of them has the satisfiability problem NP-complete. Then, we show that the modal logic S5 can be formalized in (TLQSR)^3.