=Paper=
{{Paper
|id=None
|storemode=property
|title=On the
Elimination of Quantifiers through Descriptors in
Predicate Logic
|pdfUrl=https://ceur-ws.org/Vol-857/paper_f02.pdf
|volume=Vol-857
|dblpUrl=https://dblp.org/rec/conf/cilc/CantoneAO12
}}
==On the
Elimination of Quantifiers through Descriptors in
Predicate Logic==
https://ceur-ws.org/Vol-857/paper_f02.pdf
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