A survey of computable set theory

Abstract

This paper surveys various decidability results in the set theory. In the first part, we focus on certain classes of unquantified set-theoretic formulae involving the relations ∊ “membership”, = “equality”, and the operators ⋂ “intersection”, ⋃ “binary union”, \ “set difference”, ⋅ “singleton”, pow “powerset”, Un“general union”, η “choice operator”, etc. The unquantified theory basic to the results presented is the so called Multilevel Syllogistic (MLS) which is the set of all quantifier-free formulae in the language ∊, =, ⋂, ⋃ ,\ .

The second part of the paper covers the quantified case and, among others, we consider: a quantified version of MLS, the class of formulae quantified over sets in which the membership predicate is not allowed, the class of prenex set-theoretic formulae having three quantifiers and the class having a prefix of the form ∀∀ ... ∀∃ .

In the third part, some applications to domains different from pure set theory will be reviewed.

Some undecidability results will be discussed in the last section.

An appendix on Zermelo-Fraenkel set-theory concludes the paper.