Towards tableau-based decision procedures for non-well-founded fragments of Set Theory

Abstract

We propose a tableau-like decision procedure for deciding the finite satisfiability of unquantified formulae with (a weak form of) powerset constructor. Our results apply to a rather large class of nonwell-founded set theories. The decidability result presented can be seen as a first step towards the decidability of the class of formulae into which the □-as-P (box-as-powerset) translation maps modal formulae. The analysis we make clarifies some of the difficulties in deciding this class of formulae in the case without atoms. The procedure we define can be used as a subroutine to decide the same class of formulae in Set Theory without foundation. © Springer-Verlag Berlin Heidelberg 2000.