We consider classes A,B of sentences in the restricted predicate calculus (without equality). The class A consists of all sentences that contain only valence one predicate symbols and have the quantifier prefix ∀∃∃ in their prenex normal form; class B sentences have a quantifier prefix ∀x∃y₁∃y₂∀z, contain only valence two predicate symbols and contain no atomic formulas matching P(z,x), P(z,y₁), P(z,y₂). Denote by Sat(A) (respectively Sat(B)) the set of all satisfiable sentences in the class A (class B), and by DT(T(n)) - the class of sets that can be decided by a single tape deterministic Turing machine in T(n) steps. We prove that for appropriately chosen constants a>b>1 holds
Sat(A) ∈ DT(a^n/logn)\DT(b^n/logn), Sat(A) ∈ DT(a^an/logn)\DT(b^bn/logn).

complexity of decision problem, restricted predicate calculus

Mathematical problems and theory of numerical methods