Reconciling transparency, low Δ0-complexity and axiomatic weakness in undecidability proofs

In a first-order theory Theta, the decision problem for a class of formulae Phi is solvable if there is an algorithmic procedure that can assess whether or not the existential closure of phi(there exists) of phi belongs to Theta, for any phi is an element of Phi. In 1988, Parlamento and Policriti already showed how to tailor arguments a la Godel to a very weak axiomatic set theory, referring them to the class of Sigma(1)- formulae with (for all there exists for all)(0)-matrix, i.e. existential closures of formulae that contain just restricted quantifiers of the forms (for all x is an element of y) and (there exists x is an element of y) and are writable in prenex form with at most two alternations of restricted quantifiers (the outermost quantifier being a 'for all'). While revisiting their work, we show slightly less weak theories under which incompleteness for recursively axiomatizable extensions holds with respect to existential closures of (for all there exists)(0)-matrices, namely formulae with at most one alternation of restricted quantifiers.