On the elimination of quantifiers through descriptors in predicate logic

We present a variant of the Davis--Fechter's technique for eliminating quantifiers in first-order logic, aimed at reducing the incidence of irrelevant dependencies in the construction of Skolem terms. The basic idea behind this contribution is to treat as a single syntactic unit every maximal `quantifier batch', i.e., group of contiguous alike quantifiers, whose internal order (which has no significance) is thereby prevented from entangling the final result. Through concrete cross-translations, our version of the free-variable predicate calculus turns out to be equipollent---in means of expression and of proof---to the one originally proposed by Davis and Fechter and hence to a relatively conventional version of quantified first-order logic.