On the reduction of the decision problem

Abstract

In the first paper of the above main title, one of us has proved that any formula of the first order predicate calculus is equivalent (as to being satisfiable or not) to some binary first order formula having a prefix of the form (Ex₁)(x₂)(Ex₃) … (x_n) and containing a single predicate variable. This result is an improvement of a theorem of Ackermann stating that any first order formula is equivalent to another with a prefix of the above form but saying nothing about the number of predicate variables appearing therein. Hence the question arises if other theorems reducing the decision problem to the satisfiability question of the first order formulas with a prefix of a special form can be improved in like manner. In the present paper we shall answer this question concerning Gödel's reduction theorem stating that any first order formula is equivalent to another the prefix of which has the form