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

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 tailor arguments à la Gödel to a very weak axiomatic set theory, referring them to the class of -formulae with -matrix, i.e. existential closures of formulae that contain just restricted quantifiers of the forms and and are writable in prenex form with at most two alternations of restricted quantifiers (the outermost quantifier being a ''). While revisiting their work, we show slightly less weak theories under which incompleteness for recursively axiomatizable extensions holds with respect to existential closures of -matrices, namely formulae with at most one alternation of restricted quantifiers.