We solve the satisfiability problem for a three-sorted fragment of set theory (denoted ), which admits a restricted form of quantification over individual and set variables and the finite enumeration operator {-,-,...,-} over individual variables, by showing that it enjoys a small model property, i.e., any satisfiable formula ψ of has a finite model whose size depends solely on the length of ψ itself. Several set-theoretic constructs are expressible by -formulae, such as some variants of the power set operator and the unordered Cartesian product. In particular, concerning the latter construct, we show that when finite enumerations are allowed, the resulting formula is exponentially shorter than in their absence.

The Decision Problem for a Three-sorted Fragment of Set Theory with Restricted Quantification and Finite Enumerations.

CANTONE, Domenico;NICOLOSI ASMUNDO, MARIANNA
2016

Abstract

We solve the satisfiability problem for a three-sorted fragment of set theory (denoted ), which admits a restricted form of quantification over individual and set variables and the finite enumeration operator {-,-,...,-} over individual variables, by showing that it enjoys a small model property, i.e., any satisfiable formula ψ of has a finite model whose size depends solely on the length of ψ itself. Several set-theoretic constructs are expressible by -formulae, such as some variants of the power set operator and the unordered Cartesian product. In particular, concerning the latter construct, we show that when finite enumerations are allowed, the resulting formula is exponentially shorter than in their absence.
Satisfiability problem ; restricted quantification ; set theory
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/20.500.11769/39890
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 1
social impact