Restricted Positive Quantification Is Not Elementary
Schubert, Aleksy, Paweł Urzyczyn, Daria Walukiewicz-Chrząszcz · DROPS (Schloss Dagstuhl – Leibniz Center for Informatics) · 2015
We show that a restricted variant of constructive predicate logic with positive (covariant) quantification is of super-elementary complexity. The restriction is to limit the number of eigenvariables used in quantifier introductions rules to a reasonably usable level. This construction suggests that the known non-elementary decision algorithms for positive logic may actually be best possible.