Global Skolemization with Grouped Quantifiers.
Domenico Aldo Cantone, Marianna Nicolosi Asmundo, Eugenio Giovanni Omodeo · APPIA-GULP-PRODE · 1997
When ‘local’ Skolemization treats proper axioms along with the premisses and the negated conclusion of a conjecture, each sentence originates a finite number of Skolem symbols, without any explicit connection among symbols originating from different sentences. A global approach, proposed by Davis and Fechter, consists in the simultaneous introduction of infinitely many new functors, which eliminates all quantifiers of the language in a single shot. Two conflicting goals in this elimination process are: to keep as small as possible the collection of ‘key’ formulae that deserve their own Skolem functors, and to avoid time-consuming simplifications during Skolemization. Some initial contribution is given here to this potentially open-ended research topic. A technique is proposed by which: contiguous alike quantifiers are treated as a single bunch, so as to lower the arity of Skolem functors; and their relative order —which is immaterial— does not affect the result.