Very Weak, Essentially Undecidable 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