A derived algorithm for evaluating ɛ-expressions over abstract sets

AbstractFour weak theories of pure sets are axiomatically characterized. A decision method is given for checking sentences of the form ∀y1…∀yn∃xp, where n varies over natural numbers and p over unquantified matrices, for provability in each theory. Dually, the method can be used to check ∃y1…∃yn∀x¬p for satisfiability. The completeness proof is fully constructive: this means that given a satisfiable constraint of the form ∃y1…∃yn∀x¬p, a computable model of the axioms which also fulfills the constraint can be synthesized. In this sense, we have a way of automatically generating a concrete representation of the abstract data-type “set” under varying axioms.The problem is also addressed of how to determine ɛ x p; i.e., how to find a ζ fulfilling p(ξ1,…,ξn,ζ) in a computable model M of one of our theories, as a function of input M-sets ξ1,…,ξn. A partial solution to this problem is supplied, which works when ∀y1…∀yn∃xp is a theorem and M meets a suitable condition which happens to be satisfied by those models that are produced by our automatic synthesis algorithm. A stronger condition on M is also characterized that makes ɛ x p computable in all cases (at worst through a blind search method).Examples showing the expressive power of the ∃*∀-constraints and the usefulness of ɛ-expressions in set computations are included. Envisaged extensions of the proposed methods to axiomatic set theories antithetic to the classical ones are briefly hinted at