Eigenvariables, bracketing and the decidability of positive minimal predicate logic (Q2503325)

Positive formulas of predicate logic considered here are constructed from atomic formulas by \(\&,\to,\forall\) in such a way that all occurrences of \(\forall\) are positive. The authors give a new proof of the result by the reviewer [Proc. Steklov Inst. Math. 98, 135--145 (1968; Zbl 0208.01101); translation from Tr. Mat. Inst. Steklova 98, 121--130 (1968; Zbl 0179.01102)] that the derivability problem for such formulas in the intuitionistic logic is decidable. As a consequence a new proof of decidability of the inhabitation problem for positive types in system F is obtained. The new proof like the old one establishes that every sufficiently high derivation \(d\) contains a pair of sequents, \(S\), \(S'\), such that \(S'\) is situated above \(S\) but can be contracted to \(S\) by some substitution for variables. In this case the derivation \(d\) can be simplified by (making the substitution and) throwing away the part between \(S'\) and \(S\). Now this is done by introducing a scoping mechanism into cut-free rules and proving the new formulation has a kind of a subformula property. In the reviewer's opinion, the proof is still not transparent enough. Scoping looks like replacement of universal quantifiers (in the conclusion) by existential quantifiers (in the premise). According to a recent result by Baaz and Iemhof positive existential quantifiers admit Skolemization in intuitionistic logic with the existence predicate. This is probably enough to prove decidability for formulas with only such quantifiers. It is to be seen whether these considerations allow one to simplify the author's proof.