On the reduction of the decision problem. Third paper. Pepis prefix, a single binary predicate
It has been proved by Pepis that any formula of the first-order predicate calculus is equivalent (in respect of being satisfiable) to another with a prefix of the formcontaining a single existential quantifier. In this paper, we shall improve this theorem in the like manner as the Ackermann and the Gödel reduction theorems have been improved in the preceding papers of the same main title. More explicitly, we shall prove theTheorem 1. To any given first-order formula it is possible to construct an equivalent one with a prefix of the form (1) and a matrix containing no other predicate variable than a single binary one.An analogous theorem, but producing a prefix of the formhas been proved in the meantime by Surányi; some modifications in the proof, suggested by Kalmár, led to the above form.