On the elimination of quantifiers through descriptors in predicate logic⋆ Domenico Cantone1 , Marianna Nicolosi Asmundo1 , and Eugenio G. Omodeo2 1 Dipartimento di Matematica e Informatica, Università di Catania email: cantone@dmi.unict.it, nicolosi@dmi.unict.it 2 Dipartimento di Matematica e Geoscienze, Università di Trieste email: eomodeo@units.it Abstract. We present a variant of the Davis–Fechter’s technique for eliminating quantifiers in first-order logic, aimed at reducing the inci- dence of irrelevant dependencies in the construction of Skolem terms. The basic idea behind this contribution is to treat as a single syntac- tic 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 pred- icate 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. Keywords: Hilbert’s ε-descriptor, global Skolemization, quantifier-elimination. 1 Introduction Elimination of quantifiers from formulae of first-order logic is a process that has important implications for the automated deduction field [12, 2, 5] and in foundational issues [10, 13]. When no particular theory is focussed upon, quantifiers are usually elimi- nated by adopting as tool either Skolemization or Hilbert’s ε-descriptor. Traditionally, Skolemization and the ε-symbol have been exploited differently, in somewhat complementary rôles. Skolemization is the most basic and widespread technique used to expunge existential quantifiers from automated proofs [12], one’s rationale for effacing them being the relative ease with which Skolem terms (namely, terms whose lead functor is a Skolem symbol) can be manipulated in deductions. These can in fact be treated, both at the syntactic and at the semantic level, very much like the terms of the initial language. Skolem terms are generally forgetful of the formulae from which they stem and of the context in which they are introduced. This may be of hindrance, ⋆ Work partially supported by the INdAM/GNCS 2012 project “Specifiche in- siemistiche eseguibili e loro verifica formale”. though, because it is plausible that information potentially crucial for the auto- matic discovery of shorter proofs dwells in relationships among Skolem terms. On the other hand, descriptions assembled by means of the ε-operator, the so called ε-terms, remain tied to the formulae which are the scopes of their descriptors: this is why they are so useful in investigations about foundational issues [10, 11], non-classical logics [8], and linguistics [14]. However, ε-terms are less well-suited for automation because of their elaborate structure. In [6], Davis and Fechter propose a quantifier-elimination technique which bridges Skolemization with the ε-operator. It comes along with a free-variable calculus, provably equipollent to the standard predicate calculus; unlike in stan- dard predicate calculus, in [6] quantifiers have the mere status of abbreviations, as they are reducible to suitable Skolem terms. These terms, offering a (func- tional) definition of the ε-terms, are constructed in such a way that structurally similar formulae share the same Skolem symbol. More precisely, Davis–Fechter’s technique singles out certain formulae of the language, called key formulae, to each of which it associates a function symbol uniquely. Any other formula of the language owns a specific key formula, from which it inherits a Skolem symbol. Through key formulae, [6] succeeds in providing a simultaneous translation of all formulae ϕ of a language LΣ of standard predicate logic into free-variable formulae ϕ∗ over a rich signature Σsko . This signature results from a countable infinity of Skolem augmentations of the original signature Σ, and from an overall final amalgamation step. Thanks to the plenitude of the amalgamated language, the quantifiers of any input formula ϕ can get counterpart Skolem terms in- side the translated formula ϕ∗ , whose Skolem symbols are enacted to faithfully represent them in all regards by suitable axioms, named ε-formulae. In this paper we present a variant of the Davis–Fechter’s technique, allowing one to treat contiguous alike quantifiers as a single ‘batch’. This version is based on a generalized notion of key formula, enabling one to associate several Skolem functions, independent of one another, with the same key formula. The resulting Skolem terms may be less deep and give rise to shorter proofs. We illustrate with an example the results of applying Skolemization, ǫ-operator, the Davis-Fechter technique, and our variant to a valid formula. Our variant free-variable calculus can be proved equipollent to Davis and Fechter’s original one, and hence to standard predicate logic. 2 Preliminaries We recall here some basic notions, notation and terminology used in the paper. Let LΣ be the first-order language based on: a signature Σ = (P, F ), where P (non-void) and F are finite or denumerable collections of predicate symbols and function symbols (each endowed of a fixed arity), respectively; a fixed count- able collection Vars of individual variables; the propositional connectives (say & , ∨, ¬, and ⊃, for specificity); the (infinitely many) quantifiers ∃ x and ∀ x corresponding to the individual variables x ∈ Vars. 2 Later on, various other first-order languages LΣ ′ will enter into our discus- sion, whose formation rules will be the same as for the LΣ just outlined. We will designate by L⌣Σ ′ the sublanguage resulting from each one of these by withdrawal of the quantifiers formation rule. Throughout, we use the Greek letters ϕ, ψ, χ, κ as metavariables ranging over the formulae of LΣ ; Q, P, R and g, f as metavariables ranging over predicate and function symbols, respectively; t, s, d, θ as metavariables ranging over first-order terms; and x, y, z as metavariables ranging over the individual variables. Terms and formulae are constructed according to the standard rules; likewise, the notions of syntax tree of a well-formed expression (i.e., a term or a formula; in short, wfe), of atomic formulae, of literals, of (immediate) subformulae of a given formula, of free and bound variables,, of closed formulae (sentences), of lead symbol, and so on, are as usual. Precise definitions can be found in [9, 7]. Occurrences and positions. A wfe E occurs within a wfe F at position ν, where ν is a node in the syntax tree TF of F , if the subtree of TF rooted at the node ν is identical to the syntax tree of E. In such a case, we also say that the node ν is an occurrence of E (and also an occurrence of the lead symbol of E) in F and that the path from the root of TF to ν is its occurrence path. An occurrence of E within F can be conveniently coded by a sequence over the set N+ of all positive integers,3 representing the positions within its siblings of each node in the occurrence path. Specifically, the set Pos(F ) of the positions in (the syntax tree of) any wfe F can be defined recursively as follows: 1. the empty word λ is in Pos(F ); 2. let f be a function symbol of arity n in F , and t1 , . . . , tn be terms: if F = f (t1 , . . . , tn ) and π ∈ Pos(ti ), for some i ∈ {1, . . . , n}, then i · π ∈ Pos(F );4 3. let R be a predicate symbol of arity n in P, and t1 , . . . , tn be terms: if F = R(t1 , . . . , tn ) and π ∈ Pos(ti ), for some i ∈ {1, . . . , n}, then i · π ∈ Pos(F ); 4. if F = ϕ1 ◦ ϕ2 , where ◦ ∈ { & , ∨, ⊃}, and π ∈ Pos(ϕi ), for some i ∈ {1, 2}, then i · π ∈ Pos(F ); 5. if F = ¬ψ, or F = (∃x)ψ, or F = (∀x)ψ, and π ∈ Pos(ψ), then 1 · π ∈ Pos(F ). Given any wfe F , the occurrences at given positions of subformulae or subterms of F in F are determined as follows. We put F |λ = F . In case F is a term f (t1 , . . . , tn ) or an atomic formula R(t1 , . . . , tn ), we put F |i·π = ti |π for i ∈ {1, . . . , n}. If F = ϕ1 ◦ ϕ2 , with ◦ ∈ { & , ∨, ⊃}, we put F |i·π = ϕi |π , for i ∈ {1, 2}. Finally, if F = ¬ψ, or F = (∀x)ψ, or F = (∃x)ψ, then F |1·π = ψ|π . Thus the label of a node ν at position π in the syntax tree TF of a wfe F (denoted lbl (F, π)) is the lead symbol of F |π . For example, the positions in the formula ϕ = P (x, y) & Q(f (w, w)) form the set Pos(ϕ) = {λ, 1, 2, 1·1, 1·2, 2·1, 2·1·1, 2·1·2}. The occurrence of ϕ within itself is coded by λ. ϕ|1 denotes P (x, y), ϕ|2·1 denotes f (w, w), and ϕ|2·1·1 , ϕ|2·1·2 denote two different occurrences of the same term w. 3 The set of all words over the ‘alphabet’ N+ will be designated (N+ )∗ . 4 The expression π1 · π2 denotes the concatenation of the sequences π1 and π2 . 3 Given two positions π1 , π2 ∈ Pos(F ) in a wfe F , we write π1 ⊑ π2 to indicate that π1 is a prefix of π2 , i.e. π2 = π1 · η for some η ∈ (N+ )∗ . Similarly, we write π1 < π2 when π1 is a proper prefix of π2 , i.e. π1 ⊑ π2 and π1 6= π2 . If π1 is a (proper) prefix of π2 , then F |π2 is a (proper) subexpression of F |π1 . F We denote by ΠE the collection of all positions π ∈ Pos(F ) such that F |π = F F E. If ΠE = 1, where |S| denotes the cardinality of any set S, we may use πE to denote the position of the unique occurrence of E in F . We write ΠE and πE in case the corresponding S F is clear from the context. For a collection T of wfes, we put ΠTF =Def E∈T ΠE F . It is possible to establish a lexicographic ordering ≺ over the set Pos(ϕ) of positions in a formula ϕ such that for any π1 , π2 ∈ Pos(ϕ), if π1 < π2 , then π1 ≺ π2 ; if π · n ⊑ π1 and π · n′ ⊑ π2 , for some π ∈ (N+ )∗ and n < n′ , then π1 ≺ π2 . By the syntactic structure of formulae and terms, ≺ is a well-ordering. Therefore, we can define an operation ‘min’ which selects from any nonempty subset X of Pos(ϕ) the minimum of X relative to the ordering ≺. We also write π1  π2 to indicate that either π1 ≺ π2 or π1 = π2 . Let ϕ be a formula and let us suppose, without loss of generality, that ϕ contains as propositional connectives only ¬, & , and ∨. An occurrence ν of a wfe E within a formula ϕ is positive if the negation symbol ¬ occurs an even number of times in the occurrence path of ν deprived of its last component. Otherwise, the occurrence is said to be negative. Let F be a wfe, π a position in F , and E a wfe of the same type as F |π (that is, a formula if F |π is a formula, and a term otherwise). We indicate with F [π/E] the wfe obtained by substituting the occurrence of F |π in F at position π by E, so that we have F [π/E]|π = E. Given two wfes E and F , we write F = F (E) to stress that the occurrences of E in F play a significant rôle. Thus, for instance, if E ′ is another wfe of the same type as E, by F (E ′ ) we denote the wfe resulting from F when each occurrence of E within F is replaced by a copy of E ′ . For any formula ϕ in the language LΣ , the collection of all variables that occur free in ϕ is denoted by Free(ϕ), whereas the collection of variables that occur bound in ϕ is denoted by Bound (ϕ). We further denote by Vars(ϕ) the set of all variables appearing in ϕ. σ Substitutions. A (variable-)substitution is a mapping x 7→ xσ from Vars to the collection of all terms over (Σ, Vars) such that xσ = x holds for all but a finite number of variables x. We indicate with Supp(σ) the support of σ, namely the collection of all x ∈ Vars such that xσ 6= x. Also, given the terms t1 , . . . , tn , we denote by {x1 /t1 , . . . , xn /tn } the substitution σ such that Supp(σ) ⊆ {x1 , . . . , xn } and xi σ = ti , for i = 1, . . . , n, where x1 , . . . , xn are distinct variables. A substitution is a variable renaming if it has the form {x1 /y1 , . . . , xn /yn }, with y1 , . . . , yn pairwise distinct variables. If σ = {x1 /y1 , . . . , xn /yn } is a variable renaming, {y1 /x1 , . . . , yn /xn } is the inverse substitution of σ. Given a substitution σ and a set of variables V ⊆ Vars, the restriction of σ to V is the substitution σ V s.t. xσ V =Def xσ if x ∈ V , xσ V =Def x otherwise. 4 The action of a substitution can be extended into a mapping E 7→ Eσ, recursively defined over the wfes of LΣ as usual. A substitution σ is free for a formula ϕ, if ϕ and ϕσ have exactly the same occurrences of bound variables. 3 A variant of Davis–Fechter’s language Davis and Fechter [6] proposed a way of eliminating bound variables from first- order predicate logic by successive enlargements of the signature of the language, based on the well-known Skolemization technique, which is wholesale applied to a denumerable infinity of so-called key formulae. In what follows, we will present a variant of Davis–Fechter’s calculus, where by resorting to a revised definition of key formula, we can lower the complexity of the quantifier-elimination process. The crucial remark inspiring our proposal is that in standard first-order logic contiguous alike quantifiers can be treated as a single syntactic unit: a ‘batch’. E.g., in view of their logical equivalence, the formulae ϕ1 = (∃x)(∃y)Q(x, y) and ϕ2 = (∃y)(∃x)Q(x, y) can be replaced by (∃x, y)Q(x, y), so as to make the independency between x and y explicit, and to stress the immateriality of the order of the quantifiers (∃x) and (∃y) occurring in ϕ1 and ϕ2 . This concealment of syntactic features of only apparent significance is par- ticularly rewarding when Skolemization comes into play, because the reduction of irrelevant dependencies among quantified variables leads to the construction of less intricate Skolem terms, as well as to shorter proofs [2]. Skolemization of formulae adopting generalized quantifiers like (∃x1 , . . . , xn ) can be defined in the flavour of [12] as follows. Definition 1 (Generalized Skolemization). Let χ be a formula and let χ|π be a positive (resp., negative) occurrence of (∃x1 , . . . , xn )ϕ(x1 , . . . , xn ) (resp., (∀x1 , . . . , xn )ϕ(x1 , . . . , xn )) in χ, with π posi- tion of Pos(χ). Moreover, let y1 , . . . , ym be the free variables in χ|π , h1 , . . . , hn new m-ary function symbols, and ϕ(x1 /h1 (y1 , . . . , ym ), . . . , xn /hn (y1 , . . . , ym )) the formula resulting from the replacement in ϕ of each xi by the correspond- ing hi (y1 , . . . , ym ). Then, χ[π/ϕ(x1 /h1 (y1 , . . . , ym ), . . . , xn /hn (y1 , . . . , ym ))] is obtained from χ by a Skolemization step. Skolemization of a formula is carried out by repeatedly performing Skolemiza- tion steps till all the existential (resp., universal) quantifiers occurring positively (resp., negatively) in the formula are eliminated. While performing Skolemization of a formula through an inside-out visit, one may sometimes associate with the innermost quantifier a function symbol whose arity exceeds the need; in fact, unless the quantifiers forming a single batch are treated simultaneously, one may fail to see at the inner level that certain variables are bound at an outer level. For example, the above-displayed formulae ϕ1 and ϕ2 could be brought to quantifier-free form through Skolemization in the following way (constants being regarded as 0–ary function symbols): ϕ1 becomes Q(fx (), fy (fx ())) and ϕ2 be- comes Q(gx (gy ()), gy ()). These ground sentences would actually result from the 5 Skolemization technique proposed by Davis and Fechter; an improved Skolemiza- tion, treating x and y simultaneously and on a par, and disregarding distinctions between ϕ1 and ϕ2 , would produce the simpler result Q(ℓx (), ℓy ()). Def. 1 au- thorizes us to proceed this way, thereby leading to terms that are less deep and reflect more closely the genuine dependencies across quantified variables. We will manage things so that whenever a new function symbol arises from Skolemization, it gets drawn from an infinite repository Fsko , disjoint from F and consisting of countably many distinct function symbols of any arity. The augmented signature, to be designated by Σsko = (P, F ∪ Fsko ), will originate from the quantifier-free language L⌣Σ through successive enlargement steps cul- minating in the language L⌣ Σ . sko 3.1 Generalized key formulae We will now single out a collection of special ‘key’ formulae, which will serve us in the planned formation of Fsko . Our policy will be to associate Skolem function symbols exclusively to these formulae, so as to avoid excessive proliferation of symbols in Fsko . Key formulae must hence have a very restrained syntactic form: among others, they will be devoid of quantifiers; moreover, we will class the variables of each key formula κ into two disjoint groups: – ‘key ’ variables, whose overall number n indicates how many function symbols h1 = hκ,1 , . . . , hn = hκ,n are associated to κ, and which (in analogy to the existential variables xi of Def. 1) indicate where to ‘graft’ the corresponding Skolem terms hi ( , . . . , ); and | {z } m – ‘anonymous’ variables, occurring only once inside κ, whose overall number m will determine the common arity of the Skolem symbols hi . We will also specify at the end of this section how to extract from any given for- mula ϕ its key formula, from which ϕ will inherit its Skolem symbols and whose anonymous variables must be replaced, in order to get ϕ, by terms acting—so- to-speak—as the ‘actual parameters’ of ϕ. For this purpose it is convenient to assume that the individual variables Vars are arranged in a sequence h. . . , x−2 , x−1 , x0 , x1 , x2 , x3 , . . .i, and that the two subsequences Vars − = h. . . , x−2 , x−1 , x0 i, and Vars + = hx1 , x2 , x3 , . . .i are adopted to denote key variables and anonymous variables, respectively. When it is not necessary to insist on such a convention, we will just use the meta- variables x, y, z (possibly subscripted with natural numbers) that, as mentioned above, stand for generic variables in Vars. Most of the notions introduced in Sec. 2 for the languages of standard predi- cate logic can be referred to quantifier-free languages as well. However, in absence of bound variables, Free(ψ) = Vars(ψ) holds for every formula ψ. Since variables in Vars − play a key rôle which will be highlighted in the rest of this section, we define the degree deg(ϕ) of a formula ϕ to be the cardinality Vars(ϕ) ∩ Vars − . 6 As mentioned earlier, in standard first-order logic a substitution σ is free for a formula ψ if it does not change the occurrences of bound variables in ψ. Since quantified variables are not subject to substitutions, one only has to make sure that when a variable x is replaced by a term, no variable y of the term is such that x occurs free within the scope of a quantifier binding y within ψ. An analogous concept can be given in the free-variable language, by intro- ducing the notion of substitution σ free for ψ relative to a set B ⊆ Vars, where the variables in B are treated as bound variables. More precisely, we have the following definition. Definition 2. Given a quantifier-free formula ψ, a substitution σ is said to be free for ψ relative to B ⊆ Vars if Supp(σ) ∩ B = ∅ and for each x ∈ Supp(σ) ∩ Vars(ψ) the term xσ contains none of the variables in B. Next we give the notion of most general formula relative to a set of variables. Definition 3. Let ψ and ϕ be quantifier-free formulae and let B ⊆ Vars. We say that ψ is more general than ϕ relative to B, if ϕ = ψσ for some substitution σ free for ψ relative to B. ψ is most general relative to B if whenever a formula ψ ′ is more general than ψ relative to B, then ψ is also more general than ψ ′ relative to B. Most general formulae can be characterized in merely syntactical terms as stated by the next lemma, whose proof can be found in [4]. Lemma 1. A formula ψ is most general relative to a set of variables B if and only if it satisfies the conditions: 1. any variable in Vars(ψ) \ B has exactly one occurrence in ψ; 2. any term occurring in ψ either contains a variable of B or is itself a variable, not necessarily in B. It can be checked that when two formulae ψ and ϕ are most general relative to a common set of variables B, and each one is more general than the other (relative to B), then they solely differ by a renaming of their variables not belonging to B. The latter remark yields a criterion for grouping most general formulae into equivalence classes. To set also a criterion for choosing a representative member from each of such classes, we give the following definition. Definition 4. A formula κ is a key formula if the following holds: 1. κ is most general relative to {x0 , x−1 , . . . , x1−n } ⊆ Vars(κ), for some n > 1, and min(Πx0 ) ≺ · · · ≺ min(Πx1−n ); 2. Vars(κ) \ {x0 , . . . , x1−n } = {x1 , . . . , xm }, for some m > 0, |Πxi | = 1, for i = 1, . . . , m, and πx1 ≺ · · · ≺ πxm . Consider the formula ϕ1 = P (x0 , x−1 , x1 , x2 ). Clearly it satisfies points 1 and 2 of Def. 4 and, therefore, it is a key formula. On the other hand, ϕ2 = P (x0 , x−1 , x1 , x1 ) and ϕ3 = P (x0 , x−1 , f (x1 ), x1 ) are not key formulae because they are not most general relative to {x0 , x−1 } and they do not satisfy point 2 of 7 Def. 4. Note that our key formulae of degree n = 1 coincide with key formulae as defined in [6]. Now that key formulae—the only formulae associated with Skolem symbols—have been characterized, we need to relate them to the other formulae of the language in order to be able to Skolemize any quantified formula. The idea is that any formula (∃x1 , . . . , xk )ϕ of standard predicate logic can be related to a key formula ψ and borrow its Skolem symbols in order to determine Skolem terms suitably replacing the quantified variables x1 , . . . , xk . Next we show how to relate key formulae with other formulae of the same language. Specifically, we show how, given a quantifier-free formula ϕ and a set of terms T (in principle we can consider any type of term, but for our purposes we will focus on variables and Skolem terms) we are able to effectively determine a key formula ψ and a substitution σ such that ϕ = ψσ. This result turns out to be useful several times in this paper: for example in Sec. 3.2, where we define quantifier batches, and in Sec. 4, where we introduce translation maps from standard predicate logic to the considered quantifier-free predicate logics. Let ϕ be a quantifier-free formula of a first-order language LΣ and let T be a nonempty set of terms occurring in ϕ. We start by singling out the collection KTϕ of the positions of the ⊑-minimal occurrences of the terms of T in (the syntax tree Tϕ ) of ϕ. More precisely, KTϕ is the collection of the ⊑-minimal positions in ΠTϕ , i.e., KTϕ = {π ∈ ΠTϕ | there is no π ′ ∈ ΠTϕ such that π ′ < π} . In the following, terms at such positions will be substituted with key variables whose indices depend on a rank function ι : KTϕ → N (which we will soon extend to other positions of ϕ as well), where, for π ∈ KTϕ , ι(π) is the number of distinct terms in T having some ⊑-minimal occurrence which precede, n with respect to , the first o occurrence of the term ϕ π ; in symbols, ι(π) =Def ϕ π′ : π ′ ∈ KTϕ | π ′  π ∗ , where π ∗ = Def min{π ′′ ∈ KTϕ | ϕ π′′ = ϕ π }. We put tι(π) = Def ϕ π ; then our understanding is that the term tι(π) at position π ∈ KTϕ in ϕ is to be substituted with the key variable x1−ι(π) . Let n = {ϕ π : π ∈ KTϕ } . Then we plainly have {t1 , . . . , tn } ⊆ T . When {t1 , . . . , tn } = T , we say that T is independent w.r.t. ϕ; in such a case, any term t ∈ T must have at least one occurrence in ϕ which is not contained in any occurrence in ϕ of any other term t′ ∈ T . Next, let Aϕ T be the set of the ⊑-minimal positions of subterms in ϕ which are not ⊑-comparable with any of the positions in ΠTϕ , where two positions π and π ′ in ϕ are ⊑-comparable if either π ⊑ π ′ or π ′ ⊑ π holds, and let m = |Aϕ T |. Plainly, Aϕ T ∩ K ϕ T = ∅. We extend the rank function ι on any π ∈ Aϕ T by putting ι(π) =Def {π ′ ∈ Aϕ ′ ϕ T | π  π} , i.e., ι(π) is the rank of π, within AT , in a left- to-right scan of the syntax tree of ϕ. Much as before, we also put t′ι(π) =Def ϕ π , for π ∈ Aϕ ′ T . Then our understanding is that the term tι(π) at position π in ϕ is to be substituted by the anonymous variable xι(π) . Thus, let ψ be the formula obtained by simultaneously substituting in ϕ each term tι(π) at position π ∈ KTϕ in ϕ with the key variable x1−ι(π) and each term t′ι(π′ ) at position π ′ ∈ Aϕ T in ϕ with the anonymous variable xι(π) , i.e., ψ =Def ϕ[π/x1−ι(π) ]π∈KϕT [π/xι(π′ ) ]π′ ∈AϕT . It can easily be checked that the positions in ψ containing variable occurrences are exactly those in KTϕ ∪ Aϕ T. 8 More precisely, we have Πxψ1−ι(π) = Πtϕι(π) ∩ KTϕ , for π ∈ KTϕ , (1) Πxψι(π′ ) = {π ′ } , for π ′ ∈ Aϕ T . (2) In view of Lemma 1 and the definition of the rank function ι over the positions in KTϕ , (1) and (2) imply that ψ is a key formula of degree n = {ϕ π : π ∈ KTϕ } , 5 (3) which we call the key formula of ϕ relative to T and denote by Key(ϕ, T ). Additionally, if we put σ =Def {x0 /t1 , x−1 /t2 , . . . , x1−n /tn , x1 /t′1 , . . . , xm /t′m } , then, by construction, we have immediately that ϕ = ψσ . (4) Conditions (1)-(4) characterize the key formula of ϕ relative to T . In fact, it can easily be shown that if ψ ′ is a key formula of degree {ϕ π : π ∈ KTϕ } such that ′ Πxψ1−ι(π) = Πtϕι(π) ∩ KTϕ , for π ∈ KTϕ , and ′ Πxψι(π′ ) = {π ′ } , for π ′ ∈ Aϕ T . and σ ′ is a substitution such that ϕ = ψ ′ σ ′ , then ψ ′ is the key formula of ϕ relative to T , i.e., ψ ′ coincides with Key(ϕ, T ). 3.2 Definition of quantifier batches We are now ready to define quantifiers in a way which generalizes their definition as given in [6]. When viewed as a single syntactic unit (Q x1 , . . . , xn ), a tuple Q x1 · · · Q xn of consecutive alike quantifiers (where Q ∈ {∃, ∀}) will be called a quantifier batch. Let ϕ be a quantifier-free formula and let {x1 , . . . , xn } ⊆ Vars(ϕ). The quan- tified forms (∃x1 , . . . , xn )ϕ and (∀x1 , . . . , xn )ϕ are rendered in the quantifier-free language as follows. Let ψ(x0 , . . . , x1−n , x1 , . . . , xm ) =Def Key(ϕ, {x1 , . . . , xn }) be the key formula of ϕ relative to {x1 , . . . , xn } such that Vars(ψ) = {x0 , . . . , x1−n , x1 , . . . , xm }, and let σ be a companion substitution such that ϕ = ψσ. We define the quantifiers ∃ and ∀ as the following shorthands (∃x1 , . . . , xn )ϕ ≡Def ψ(hψ,1 (x1 , . . . , xm )σ, . . . , hψ,n (x1 , . . . , xm )σ, x1 σ, . . . , xm σ), (∀x1 , . . . , xn )ϕ ≡Def ψ(h¬ψ,1 (x1 , . . . , xm )σ, . . . , h¬ψ,n (x1 , . . . , xm )σ, x1 σ, . . . , xm σ), where the hψ,i ’s and the h¬ψ,i ’s are the distinct symbols uniquely associated with ψ and ¬ψ, respectively, as hinted at the beginning of Sec. 3.1 (further clarifications are postponed to Sec. 3.3). 5 In particular, when T is independent w.r.t. ϕ, we have n = |T |. 9 Let us momentarily denote by ϕ∃ the definiens (just given) of (∃x1 , . . . , xn )ϕ and by ϕ∀ the analogous definiens of (∀x1 , . . . , xn )ϕ; so we can say that the quantifier batches (∃x1 , . . . , xn ) and (∀x1 , . . . , xn ) appearing in the original ϕ have ‘concretized’ into the n-tuples – hhψ,1 (x1 , . . . , xm )σ, . . . , hψ,n (x1 , . . . , xm )σi and – hh¬ψ,1 (x1 , . . . , xm )σ, . . . , h¬ψ,n (x1 , . . . , xm )σi of Skolem terms appearing in ϕ∃ and in ϕ∀ , respectively. Looking at each Skolem term more closely, we can say that the term hψ,j (x1 , . . . , xm )σ concretizes in ϕ∃ that one component xk of (∃x1 , . . . , xn ) for which x1−j σ = xk holds. Like- wise, the Skolem term h¬ψ,j (x1 , . . . , xm )σ concretizes in ϕ∀ the component xk of (∀x1 , . . . , xn ) for which x1−j σ = xk holds. Example 1. The free-variable rendering of (∃x, y)Q(x, y) is Q(hQ,1 (), hQ,2 ()), with hQ,1 () and hQ,2 () the 0-ary Skolem functions associated with the key for- mula Q(x0 , x−1 ) of degree 2 of Q(x, y) relative to T = {x, y}. Compare this with the quantifier-free translations of ϕ1 and ϕ2 discussed after Def. 1: hQ,1 () and hQ,2 () match the third and best rendering of (∃x, y)Q(x, y) examined there. When ψ is a key formula of degree 1, we often prefer to denote its corresponding Skolem function symbol with hψ rather than with hψ,1 . 3.3 The augmented signatures and their amalgamation In the light of the notions introduced in Sec. 3, we are ready to define the completed signature Σsko , on which our quantifier-free language L⌣ Σsko is based. Starting with the initial signature Σ = (P, F ) of our language, we define the following hierarchy of augmented signatures: – F0 =Def F and Σ0 =Def Σ. – For i > 1, • Fi is the set comprising exactly one symbol hψ,j new to Σi−1 , for each pair (ψ, j) with 1 6 j 6 n and ψ a key formula of L⌣ Σi−1 of degree n > 1 ⌣ ′ not belonging to any LΣi′ for which i < i − 1. The arity of hψ,j equals |Vars(ψ)| − n; • Σi =Def (P, Fi ). S∞ S∞ – To end, put Fsko =Def i=1 Fi and Σsko =Def (P, i=0 Fi ) . We also define the notion of rank of a wfe of L⌣ Σ , Skrank (·), as follows: sko Skrank (E) =Def min{k ∈ N : E is in the language L⌣ Σk }. 4 Cross-translation tools In considering now the quantified version LΣsko of the L⌣ Σsko constructed so far, we will assume, for the sake of simplicity and without loss of generality, that all quantifiers are maximally generalized in the sense that LΣsko contains no formulae like (∃x, y)(∃z)P (x, y, z), but only formulae like (∃x, y, z)P (x, y, z). 10 First translation of the standard predicate language LΣsko into the free-variable ∗ language L⌣ Σsko . In [6], Davis and Fechter defined a translation map (·) : ⌣ LΣsko → LΣ , leading from standard predicate logic to free-variable languages sko via the exploitation of key formulae of degree 1 for defining quantifiers. The translation map (·)∗ preserves the structure of wfes and acts only on formulae χ = (Qx1 , . . . , xn )ϕ with Q ∈ {∃, ∀}. It is recursively defined as follows:  ∗ − → ∗ ϕ  {xn /h±ψn (sn )} ∗ if n = 1, χ = − →  (Qx1 , . . . , xn−1 )ϕ∗ {xn /h±ψn (sn )} otherwise, where - ψn = Key(ϕ∗ , {xn }), - ±ψn = if (Q = ∃) then ψn else ¬ψn fi, - σn is such that ϕ∗ = ψn σn , - − s→ → − n = xn σn , −→ - xn = hx1 , . . . , xmn i, with x1 , . . . , xmn the variables in Vars(ψn ) \ {x0 }. ∗ ∗ We indicate with [L⌣ Σsko ] the set of the images of the map (·) . The following example illustrates how a formula of standard predicate logic can be translated into quantifier-free form via (·)∗ . Example 2. Let χ = (∃x, y, z)P (x, y, z) and put ϕ4 = P (x, y, z). Then by a first recursionstep we obtain ∗  ∗ χ∗ = (∃x, y)ϕ∗ {z/h (− 4 → s )} = (∃x, y)P (x, y, h (x, y)) , ψ3 3 ψ3 s3 = − where ψ3 = Key(ϕ4 , {z}) = P (x1 , x2 , x0 ), → − → x3 σ3 = hx1 , x2 i{x0 /z, x1 /x, x2 /y} = hx, yi. Next, put ϕ3 = P (x, y, hψ3 (x, y)). By a second recursion step, we obtain  ∗  ∗ ∗ ∗ → − χ = (∃x)ϕ3 {y/hψ2 ( s2 )} = (∃x)P (x, hψ2 (x, x), hψ3 (x, hψ2 (x, x))) , where – ψ2 = Key(ϕ3 , {y}) = P (x1 , x0 , hψ3 (x2 , x0 )), s2 = − – − → → x2 σ2 = hx1 , x2 i{x0 /y, x1 /x, x2 /x} = hx, xi. Finally, let us put ϕ2 = P (x, hψ2 (x, x), hψ3 (x, hψ2 (x, x))). Then by a last appli- cation of a recursion step we obtain χ∗ = ϕ∗2 {x/hψ1 (− → s1 )} = P (hψ1(), hψ2 (hψ1(), hψ1()), hψ3 (hψ1(), hψ2 (hψ1(), hψ1()))) , where ψ1 = Key(ϕ2 , {x}) = P (x0 , hψ2 (x0 , x0 ), hψ3 (x0 , hψ2 (x0 , x0 ))), and − → s1 = → − x1 σ1 = h i{x0 /x} = h i. Second translation of the standard predicate language LΣsko into the free-variable language L⌣ Σsko . We will now describe our proposed map for translating standard predicate languages into free-variable languages, where quantifiers are defined by means of generalized key formulae. As (·)∗ , (·)g : LΣsko → L⌣Σsko is a map preserving the structure of wfes acting only on formulae χ = (Qx1 , . . . , xn )ϕ with Q ∈ {∃, ∀}. Specifically we have that g χg = (Qx1 , . . . , xn )ϕ = ψσ ′ , where 11 g - ψ = Key(ϕ  , {x1− → , . . . , xn }), h ±ψ,j x )σ ( x = x1−j , for 1 6 j 6 n - σ ′ (x) = σ(x) otherwise - σ is such that ϕg = ψσ, - ±ψ = if (Q = ∃) then ψ else ¬ψ fi, - − →x = hx1 , . . . , xm i, where x1 , . . . , xm are the variables in Vars(ψ) \ {x0 , . . . , x1−n }. Example 3. Let us consider again the formula χ = (∃x, y, z)P (x, y, z) from Example 2. Let us put ϕ = P (x, y, z). Then we have ϕg = P (x, y, z). Let ψ = Key(ϕg , {x, y, z}) = P (x0 , x−1 , x−2 ) and let σ = {x0 /x, x−1 /y, x−2 /z}. We have ϕg = ψσ. Since ψ does not contain any anonymous variable, we have → −x = h i and σ ′ = {x0 /hψ,1 (), x−1 /hψ,2 (), x−2 /hψ,3 ()}. Therefore χg = ψσ ′ = P (x0 , x−1 , x−2 ){x0 /hψ,1 (), x−1 /hψ,2 (), x−2 /hψ,3 ()} = P (hψ,1 (), hψ,2 (), hψ,3 ()) . Notice that, much like in Example 1, no nesting of function symbols has arisen. The set of all images of the map (·)g is denote with [L⌣ Σ ]g . sko 5 The free-variable calculus, revisited Our version of the Davis–Fechter’s free-variable calculus, here denoted GVΣ , is based on the language L⌣ Σsko . Its only inference rule is modus ponens and its logical axioms are the formula schemes of L⌣ Σsko listed here: • tautologies; • identity axioms of the form t = t; • congruence axioms, of the two types: t0 = s0 & · · · & tn = sn ⊃ g( t0 , . . . , tn ) = g( s0 , . . . , sn ) , t0 = s0 & · · · & tn = sn ⊃ ( Q( t0 , . . . , tn ) ⊃ Q( s0 , . . . , sn ) ) ; • ε-formulae,  of the form  ϕ t1 , . . . , tn , d1 , . . . , dm ⊃   ϕ hϕ,1 (d1 , . . . , dm ), . . . , hϕ,n (d1 , . . . , dm ), d1 , . . . , dm , where ti s, sj s, and dk s stand for arbitrary terms, g for a function symbol of non-null arity in F ∪ Fsko , Q for a predicate symbol, ϕ for a key formula of degree n, and m equals |Vars(ϕ)| − n. Note that all of these are universally valid formulae, save the ε-formulae, which are nevertheless essential to reflect the intended meaning of the Skolem function symbols. They enter into the notion of derivability introduced below. Let ϕ and Γ be, respectively, a formula and a collection of formulae of L⌣ Σsko . We write Γ ⊢GVΣ ϕ (ϕ is derivable from Γ ), to indicate that there exists a derivation D of ϕ from Γ in GVΣ . D is a sequence ϕ1 , . . . , ϕn of formulae of L⌣Σ such that ϕn ≡ ϕ and such that each ϕi is either a tautology, or an sko 12 identity or congruence axiom, or an ε-formula, or it is obtained by means of modus ponens from ϕj , ϕk ≡ ϕj ⊃ ϕi , where j, k < i. Notice that the only difference between the above formulation GVΣ of the calculus and the very similar Davis–Fechter’s formalization VΣ (cf. [6]) lies in ∗ the languages underlying the calculi: L⌣ ⌣ Σsko for GVΣ and [LΣsko ] for VΣ . This forces us to introduce generalized ε-formulae among the axioms of GVΣ . Let TΣ be a standard predicate calculus over LΣ formalized as in [13]. It can be shown that for every formula ϕ ∈ LΣ , ⊢TΣ ϕ holds if and only if ⊢GVΣ ϕg . For space reasons we refrain from presenting the whole proof and just give some hints on how to proceed. The interested reader can find the details in [4]. The proof is worked out by relating GVΣ with VΣ and exploiting the equiv- alence result between VΣ and TΣ presented in [6]. To begin with, it can be shown that GVΣ is a conservative extension of VΣ . This means that introducing new function symbols (generated by the general- ized key formulae) and new axioms (the generalized ε-formulae) in VΣ does not increase its deductive power. The proof can be carried out by showing that any ∗ proof of ϕ in GVΣ , for a given formula ϕ of [L⌣ Σsko ] , can be translated into a proof of ϕ in VΣ , by induction on the length of the proof of ϕ in GVΣ . Next it can be proved that for every ϕ of LΣ , ⊢VΣ ϕ∗ holds if and only if ⊢GVΣ ϕg . To do this, one can first show that ⊢GVΣ ϕ∗ if and only if ⊢GVΣ ϕg and then, since GVΣ is a conservative extension of VΣ , the thesis follows. The first part of the proof can be carried out by using an appropriate function to translate ∗ any formula of L⌣ ⌣ Σsko into a formula of [LΣsko ] and a function to translate any ⌣ ⌣ g formula of LΣ into a formula of [LΣ ] . The latter function is constructed sko sko using a suitable tool, called Skolem nest, to detect Skolem terms representing contiguous alike quantifiers inside formulae of L⌣Σsko . For a description of Skolem nest and related technical details the reader is referred to [4]. Using the above result jointly with [6, Theorem 6.2], one can prove that TΣ and GVΣ are equivalent. Our variant of the free-variable calculus does not add deductive power to Davis–Fechter’s original version and, therefore, it does not add deductive power to standard predicate logic either. On the other hand, some differences may be noticed in the length of the resulting proofs. In fact, as the constructive proofs of the statements introduced in this section suggest, our variant may lead to shorter proofs. We illustrate this by means of a simple example. Example 4. Consider the valid formula ϕ = (∃x, y)Q(x, y) ⊃ (∃y, x)Q(x, y) of LΣ . The formulae obtained from ϕ by applying Skolemization, the ε-operator, the Davis-Fechter’s technique, and our variant of Davis-Fechter’s technique, are: – Skolemization: Skol(ϕ) ≡ (∃x, y)Q(x, y) ⊃ Q(h1 (), h2 ()). To prove the validity of the formula Skol(ϕ) one must instantiate the uni- versally quantified variables x and y as h1 () and h2 (), respectively. – ε-operator: Eps(ϕ) ≡ Q(εx.Q(x, εy.Q(x, y)), εy.Q(εx.Q(x, εy.Q(x, y)), y)) ⊃ Q(εx.Q(x, εy.Q(εx.Q(x, y), y)), εy.Q(εx.Q(x, y), y)). 13 Clearly the formula Eps(ϕ) looks neither easy to read nor to manipulate. – Davis-Fechter’s technique: ϕ∗ ≡ Q(hQ2 (), hQ1 (hQ2 ())) ⊃ Q(hQ3 (hQ4 ()), hQ4 ()). Validity of ϕ∗ can be proved by applying the syllogism rule to the ε-formulae: ε1 ≡ Q(hQ2 (), hQ1 (hQ2 ())) ⊃ Q(hQ3 (hQ1 (hQ2 ())), hQ1 (hQ2 ())) , ε2 ≡ Q(hQ3 (hQ1 (hQ2 ())), hQ1 (hQ2 ())) ⊃ Q(hQ3 (hQ4 ()), hQ4 ()); – our variant of Davis-Fechter’s technique: ϕg ≡ Q(hQ1,1 (), hQ1,2 ()) ⊃ Q(hQ1,1 (), hQ1,2 ()) . Notice that ϕg is a tautology of L⌣ Σ . sko 6 Conclusions and future work We have defined a variant of Davis–Fechter’s technique for eliminating quan- tifiers in first-order predicate logic, that enables treatment of contiguous alike quantifiers as a single syntactic unit. Our variant does not add deductive power to the original formalism presented in [6]. Nonetheless it makes the system more efficient, because by constructing less complex and less deep Skolem terms it allows one to obtain shorter proofs, as said in the ending remarks and example here above. Davis–Fechter’s technique has already been employed in the context of tableau systems for classical first-order logic. For instance, in [1] it has been used to define ∗ an optimized version of the delta expansion rule. Such variant, called δ∗ -rule, has the advantage of leading to non elementary speed-ups in proof length with respect to other delta-rule versions in the literature. It also yields Skolem terms that reflect in a more∗ proper way the meaning of the instantiation. The con- struction of the δ∗ -rule relies on a variant of the notion of key-formula that allows one to deal with quantifiers, inevitably present in an outer Skolemization process such as the one adopted in tableau systems by the δ-rule. Davis–Fechter’s technique also played a central rôle in [2], where a generic δ-rule based on the notion of key formula is presented, which is so designed as to ensure the correctness of any variant δ-rule to which it can be instantiated. Such a unified framework not only provides a schema apt to prove the correctness of versions of the δ-rule present in the literature, but it also enables comparisons between them that yield information on their efficiency and naturalness. In [3], the framework introduced in [2] has been applied to map in the context of standard δ-rules, a version of the δ-rule, called δε -rule, that adopts ε-terms (instead of Skolem terms) as syntactical objects to expand existentially quanti- fied formulae. The results that we present in this paper are an initial contribution to the process of analysis and improvement of the Davis–Fechter’s technique. We plan to add further refinements to the main procedure, like for instance the possibility of using, in validity (unsatisfiability) proofs, only ε-formulae rel- ative to positive (negative) occurrences of existential quantifiers in the formula under consideration. 14 We also intend to compare Davis–Fechter’s Skolem terms with ε-terms, in- vestigating their exploitations both in theoretical issues and in automated de- duction. A further development of our research concerns the application of Davis– Fechter’s technique to mathematical theories such as set theory. This will call for an adaptation of the original notion of key formula that makes it sensitive to the axioms of the theories being considered. Acknowledgments The authors wish to thank the referees for their helpful suggestions and com- ments. References 1. D. Cantone and M. Nicolosi Asmundo. A Further and Effective Liberalization of the δ-Rule in Free Variable Semantic Tableaux. In R. Caferra and G. Salzer, edi- tors, Automated Deduction in Classical and Non Classical Logic - Selected papers, volume 1761 of Lecture Notes in Artificial Intelligence, pages 109–125. Springer Verlag Berlin Heidelberg, 2000. 2. D. Cantone and M. Nicolosi Asmundo. A sound framework for δ-rule variants in free variable semantic tableaux. J. Autom. Reasoning, 38(1-3):31–56, 2007. 3. D. Cantone and M. Nicolosi Asmundo. Skolem functions and Hilbert’s ǫ-terms in Free Variable Tableau Systems. In Proceedings of CILC’06 - Italian Conference on Computational Logic, Bari, Italia, 26-27 Giugno, 2006. 4. D. Cantone, M. Nicolosi Asmundo, and E. G. Omodeo. On the elimination of quantifiers through descriptors in predicate logic (extended version), 2012. http://www.dmi.unict.it/∼nicolosi/QuantElim.pdf. 5. D. C. Cooper. Theorem proving in arithmetic without multiplication. In B. Meltzer and D. N. Michie, editors, Machine Intelligence, volume 7, pages 91–99. Edinburgh University Press, 1972. 6. M.D. Davis and R. Fechter. A free variable version of the first-order predicate calculus. J. of Logic and Computation, 1(4):431–451, 1991. 7. N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pages 243–320. 1990. 8. M. C. Fitting. A modal logic ε-calculus. Notre Dame J. of Formal Logic, 16:1–16, 1975. 9. M. C. Fitting. First-Order Logic and Automated Theorem Proving. Graduate Texts in Computer Science. Springer-Verlag, New York, 1996. second edition. 10. A.C. Leisenring. Mathematical Logic and Hilbert’s ε-symbol. MacDonald & Co., 1969. 11. G. Moser and R. Zach. The epsilon calculus and Herbrand complexity. Studia Logica, 82:133–155, 2006. 12. A. Nonnengart and C. Weidenbach. Computing small clause normal forms. In Handbook Automated Reasoning, pages 335–367. 2001. 13. J. R. Shoenfield. Mathematical Logic. Series in Logic. Addison-Wesley, 1967. 14. K. von Heusinger. Definite descriptions and choice functions. In S. Akama, editor, Logic, Language and Computation, pages 61–91, Dordrecht, 1997. Kluwer. 15