Very Weak, Essentially Undecidabile Set Theories.

In a first-order theory Θ, the decision problem for a class of formulae Φ is solvable if there is an algorithmic procedure that can assess whether or not the existential closure ϕ ∃ of ϕ belongs to Θ, for any ϕ ∈ Φ. In 1988, Parlamento and Policriti already showed how to apply G¨odel-like arguments to a very weak axiomatic set theory, with respect to the class of Σ1-formulae with (∀∃∀)0-matrix, i.e., existential closures of formulae that contain just restricted quantifiers of the kind (∀x ∈ y) and (∃x ∈ y) and are writeable in prenex form with at most two alternations of restricted quantifiers (the outermost quantifier being a ‘∀’). While revisiting their work, we show slightly stronger theories under which incompleteness for recursively axiomatizable extensions holds with respect to existential closures of (∀∃)0-matrices, namely formulae with at most one alternation of restricted quantifiers.