Decidability and Proof Procedures for Set Theory with a Choice Operator

Candidate: Omodeo,Eugenio Giovanni


Various decision algorithms are described and proved correct, each applying to a particular collection of unquantified set-theoretical formulas. Some of these algorithms are able to determine whether each given formula is satisfiable, some others can only establish whether it is satisfiable by means of an interpretation in which the values of the terms appearing in the formula are finite sets. In most cases, formulas are allowed to involve a choice operator which selects from every non-empty set s the minimum of s with respect to a well-ordering of the class of all sets. A semi-decision procedure is also described which applies to unquantified formulas in which all familiar set-theoretical operators are allowed to appear, with certain limitations imposed only on the occurrences of the unionset and choice operators. The execution of this procedure only terminates when the input formula is finitely satisfiable.