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 form
![](//static.cambridge.org/content/id/urn%3Acambridge.org%3Aid%3Aarticle%3AS0022481200103123/resource/name/S0022481200103123_equ1.gif?pub-status=live)
containing 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 the
Theorem 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 form
![](//static.cambridge.org/content/id/urn%3Acambridge.org%3Aid%3Aarticle%3AS0022481200103123/resource/name/S0022481200103123_equ2.gif?pub-status=live)
has been proved in the meantime by Surányi; some modifications in the proof, suggested by Kalmár, led to the above form.