On the reduction of the decision problem. Third paper. Pepis prefix, a single binary predicate
László Kalmár, János Surányi · Journal of Symbolic Logic · 1950
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 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 has been proved in the meantime by Surányi; some modifications in the proof, suggested by Kalmár, led to the above form.