Formative processes with applications to the decision problem in set theory: Ⅱ. Powerset and singleton operators, finiteness predicate

摘要

In an effort to marry set theory and theoretical computer science, in 1970 the Computable Set Theory project was launched to study decidable fragments of set theory. A challenging question for researchers has been finding a way to overcome the impossibility of finding finite models that do not exceed a fixed size and to solve advanced decidability problems when the list of nontrivial set constructors is lengthened. The unquantified multi-level syllogistic with singleton and powerset operators (MLSSP) is a result from this research movement. MLSSPF, the subject of this paper, extends MLSSP with the predicate Finite(x), asserting the finite cardinality of the argument.