Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized δ-Rule but

Without Skolemization

Claus-Peter Wirth

wirth@LS5.cs.uni-dortmund.de

http://LS5.cs.uni-dortmund.de/˜ wirth/welcome.html

Research Report 698/1998

http://LS5.cs.uni-dortmund.de/˜ wirth/p/gr698/all.ps.gz

December 13, 1998

Revised April 1, 1999

(Typos corrected, Proof of Lemma 5.4 and Abstract shortened, References extended)

Revised Sept. 29, 1999 (Typos corrected)

Universität Dortmund

Informatik V D-44221 Dortmund

Germany

Abstract: We present a combination of raising, explicit variable dependency representation, the liberalized δ-rule, and preservation of solutions for first-order deductive theorem proving. Our main motivation is to provide the foundation for our work on inductive theorem proving.

Contents

1 Introduction 1 1.1 Without Skolemization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Sequent and Tableau Calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.3 Preservation of Solutions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.4 The Liberalized δ-rule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

2 Basic Notions, Notations, and Assumptions 8 3 Two Versions of Variable-Conditions 9 4 The Weak Version 12 5 The Strong Version 17 6 Conclusion 28 7 The Proofs 29 References and Notes 38

1 Introduction

The paper organizes as follows: After explaining the technical terms of the title in Section 1 and the remaining basic notions in Section 2, we start to explicate the differences between our two versions of calculi in Section 3. The weak version is explained in Section 4. The changes necessary for the strong version in order to admit liberalization of the δ-rule are explained in Section 5. After concluding in Section 6 we append all the proofs, references, and notes.

1.1 Without Skolemization

In this paper we discuss how to analytically prove first-order theorems in contexts where Skolemization is not appropriate. Skolemization has at least three problematic aspects.

1. Skolemization enrichs the signature or introduces higher-order variables. Unless special care is taken, this may introduce objects into empty universes and change the notion of term-generatedness or Herbrand models. Above that, the Skolem functions occur in answers to goals or solutions of constraints^{1} which in general cannot be translated into the original signature. For a detailed discussion of these problems cf. Miller (1992).

2. Skolemization results in the following simplified quantification structure:

For all Skolem functions u⃗ there are solutions to the free existential variables e⃗ (i.e. the free variables of Fitting (1996)) such that the quantifier-free theorem T (e⃗, u⃗) is valid. Short: ∀u⃗: ∃e⃗: T (e⃗, u⃗).

Since the state of a proof attempt is often represented as the conjunction of the branches of a tree (e.g. in sequent or (dual) tableau calculi), the free existential variables become “rigid” or “global”, i.e. a solution for a free existential variable must solve all occurrences of this variable in the whole proof tree. This is because, for B_{0}, …, B_{n} denoting the branches of the proof tree,

∀u⃗: ∃e⃗: ( B_{0} ∧ … ∧ B_{n} )

is logically strictly stronger than ∀u⃗: ( ∃e⃗: B_{0} ∧ … ∧ ∃e⃗: B_{n} ).

Moreover, with this quantification structure it does not seem to be possible to do inductive theorem proving by finding, for each assumed counterexample, another counterexample that is strictly smaller in some wellfounded ordering.^{2} The reason for this is the following. When we have some counterexample u⃗ for T (e⃗, u⃗) (i.e. there is no e⃗ such that T (e⃗, u⃗) is valid) then for different e⃗ different branches B_{i} in the proof tree may cause the invalidity of the conjunction. If we have applied induction hypotheses in more than one branch, for different e⃗ we get different smaller counterexamples. What we would need, however, is one single smaller counterexample for all e⃗.

3. Skolemization increases the size of the formulas. (Note that in most calculi the only relevant part of Skolem terms is the top symbol and the set of occurring variables.)

The first and second problematic aspects disappear when one uses raising (cf. Miller (1992)) instead of Skolemization. Raising is a dual of Skolemization and simplifies the quantification structure to something like:

There are raising functions e⃗ such that for all possible values of the free universal variables u⃗ (i.e. the nullary constants or “parameters”) the quantifier-free theorem T (e⃗, u⃗) is valid. Short: ∃e⃗: ∀u⃗: T (e⃗, u⃗).

Note that due to the two duality switches “unsatisfiability/validity” and “Skolemization/ raising”, in this paper raising will look much like Skolemization in refutational theorem proving. The inverted order of universal and existential quantification of raising (compared to Skolemization) is advantageous because now

∃e⃗: ∀u⃗: ( B_{0} ∧ … ∧ B_{n} )

is indeed logically equivalent to ∃e⃗: ( ∀u⃗: B_{0} ∧ … ∧ ∀u⃗: B_{n} ).

Furthermore, inductive theorem proving works well: When, for some e⃗, we have some counterexample u⃗ for T (e⃗, u⃗) (i.e. T (e⃗, u⃗) is invalid) then one branch B_{i} in the proof tree must cause the invalidity of the conjunction. If this branch is closed, then it contains the application of an induction hypothesis that is invalid for this e⃗ and the u′ resulting from the instantiation of the hypothesis. Thus, u′ together with the induction hypothesis provides the strictly smaller counterexample we are searching for for this e⃗.

The third problematic aspect disappears when the dependency of variables is explicitly represented in a variable-condition, cf. Kohlhase (1995). This idea actually has a long history, cf. Prawitz (1960), Kanger (1963), Bibel (1987). Moreover, the use of variable-con-ditions admits the free existential variables to be first-order.

1.2 Sequent and Tableau Calculi

In Smullyan (1968), rules for analytic theorem proving are classified as α-, β-, γ-, and δ-rules independently from a concrete calculus.

α-rules describe the simple and the

β-rules the case-splitting propositional proof steps.

γ-rules show existential properties, either by exhibiting a term witnessing to the existence or else by introducing a special kind of variable, called “dummy” in Prawitz (1960) and Kanger (1963), and “free variable” in footnote 11 of Prawitz (1960) and in Fitting (1996). We will call these variables free existential variables. By the use of free existential variables we can delay the choice of a witnessing term until the state of the proof attempt gives us more information which choice is likely to result in a successful proof. It is the important addition of free existential variables that makes the major difference between the free variable calculi of Fitting (1996) and the calculi of Smullyan (1968). Since there use to be infinitely many possibly witnessing terms (and different branches may need different ones), the γ-rules (under assistance of the β-rules) often destroy the possibility to decide validity because they enable infinitely many γ-rule applications to the same formula.

δ-rules show universal properties simply with the help of a new symbol, called a “parameter”, about which nothing is known. Since the present free existential variables must not be instantiated with this new parameter, in the standard framework of Skolemization and unification the parameter is given the present free existential variables as arguments. In this paper, however, we will use nullary parameters, which we call free universal variables. These variables are not free in the sense that they may be chosen freely, but in the sense that they are not bound by any quantifier. Our free universal variables are similar to the parameters of Kanger (1963) because a free existential variable may not be instantiated with all of them. We will store the information on the dependency between free existential variables and free universal variables in variable-conditions.

1.3 Preservation of Solutions

Users even of pure Prolog are not so much interested in theorem proving as they are in answer computation. The theorem they want to prove usually contains some free existential variables that are instantiated during a proof attempt. When the proof attempt is successful, not only the input theorem is known to be valid but also the instance of the theorem with the substitution built-up during the proof. Since the knowledge of mere existence is much less useful than the knowledge of a term that witnesses to this existence (unless this term is a only free existential variable), theorem proving should—if possible—always provide these witnessing terms. Answer computation is no problem in Prolog’s Horn logic because it is so simple. But also for the more difficult clausal logic, answer computation is possible. Cf. e.g. Baumgartner & al. (1997), where tableau calculi are used for answer computation in clausal logic. Answer computation becomes even harder when we consider full first-order logic instead of clausal logic. When δ-steps occur in a proof, the introduced free universal variables may provide no information on what kind of object they denote. Their excuse may be that they cannot do this in terms of computability or λ-terms. Nevertheless, they can provide this information in form of Hilbert’s ε-terms, and the strong versions of our calculi will do so. When full first-order logic is considered, one should focus on preservation of solutions instead of computing answers. By this we mean at least the following property:

All solutions that transform a proof attempt for a proposition into a closed proof (i.e. the closing substitutions for the free existential variables) are also solutions of the original proposition.

This again is closely related to inductive theorem proving: Suppose that we finally have shown that for the reduced form R(e⃗, u⃗) (i.e. the state of the proof attempt) of the original theorem T (e⃗, u⃗) (cf. the discussion in Section 1.1), there is some solution e⃗ such that for each counterexample u⃗ of R(e⃗, u⃗) there is a counterexample u′ for the original theorem and that this u′ is strictly smaller than u⃗ in some wellfounded ordering. In this case we have proved T (e⃗, u⃗) only if the solution e⃗ for the reduced form ∀u⃗: R(e⃗, u⃗) is also a solution for the original theorem ∀u⃗: T (e⃗, u⃗).

1.4 The Liberalized δ-rule

We use ‘⊎’ for the union of disjoint classes and ‘id’ for the identity function. For a class R we define domain, range, and restriction to and image^{3} and reverse-image of a class A by

\begin{aligned}dom(R) & := & \{ a | ∃b: (a, b) ∈ R \} & ; \\ ran(R) & := & \{ b | ∃a: (a, b) ∈ R \} & ; \\ _{A}|R & := & \{ (a, b) ∈ R | a ∈ A \} & ; \\ ⟨A⟩R & := & \{ b | ∃a ∈ A: (a, b) ∈ R \} & ; \\ R⟨B⟩ & := & \{ a | ∃b ∈ B: (a, b) ∈ R \} & . \end{aligned}

We define a sequent to be a list of formulas.^{4} The conjugate of a formula A (written: \overline{A} ) is the formula B if A is of the form ¬B, and the formula ¬A otherwise. Note that the conjugate of the conjugate of a formula is the original formula again, unless it has the form ¬¬B.

In the tradition of Gentzen (1935) we assume the symbols for free existential variables (i.e. the free variables of Fitting (1996)), free universal variables (i.e. nullary parameters), bound variables (i.e. variables for quantified use only), and the constants (i.e. the function (and predicate) symbols from the signature) to come from four disjoint sets V_{∃}, V_{∀}, V_{bound}, and Σ. We assume each of V_{∃}, V_{∀}, V_{bound} to be infinite (for each sort) and set V_{free} := V_{∃}⊎V_{∀}. Moreover, due to the possibility to rename bound variables w.l.o.g., we do not permit quantification on variables that occur already bound in a formula; i.e. e.g. ∀x: A is only a formula in our sense if A does not contain a quantifier on x like ∀x or ∃x. The simple effect is that our γ- and δ-rules can simply replace all occurrences of x. For a term, formula, sequent Γ etc., ‘V_{∃}(Γ)’, ‘V_{∀}(Γ)’, ‘V_{bound}(Γ)’, ‘V_{free}(Γ)’ denote the sets of variables from V_{∃}, V_{∀}, V_{bound}, V_{free} occurring in Γ, resp.. For a substitution σ we denote with ‘Γ σ’ the result of replacing in Γ each variable x in dom(σ) with σ(x). Unless stated otherwise, we tacitly assume that each substitution σ satisfies V_{bound}(dom(σ) ∪ ran(σ)) = ∅, such that no bound variables can be replaced and no additional variables become bound (i.e. captured) when applying σ.

A variable-condition R is a subset of V_{∃} × V_{∀}. Roughly speaking, (x^{∃}, y^{∀}) ∈ R says that x^{∃} is older than y^{∀}, so that we must not instantiate the free existential variable x^{∃} with a term containing y^{∀}.

While the benefit of the introduction of free existential variables in γ-rules is to delay the choice of a witnessing term, it is sometimes unsound to instantiate such a free existential variable x^{∃} with a term containing a free universal variable y^{∀} that was introduced later than x^{∃}:

Example 1.1

∃x: ∀y: (x = y)

is not deductively valid. We can start a proof attempt via: γ-step:

∀y: (x^{∃} = y).

δ-step:

(x^{∃} = y^{∀}).

Now, if we were allowed to substitute the free existential variable x^{∃} with the free universal variable y^{∀}, we would get the tautology (y^{∀} = y^{∀}), i.e. we would have proved an invalid formula. In order to prevent this, the δ-step has to record (x^{∃}, y^{∀}) in the variable-condition, which disallows the instantiation step.

In order to restrict the possible instantiations as little as possible, we should keep our variable-conditions as small as possible. Kanger (1963) and Bibel (1987) are quite generous in that they let their variable-conditions become quite big:

Example 1.2

∃x: ( P(x) ∨ ∀y: ¬P(y) )

can be proved the following way: γ-step:

( P(x^{∃}) ∨ ∀y: ¬P(y) ).

α-step:

P(x^{∃}), ∀y: ¬P(y).

δ-step:

P(x^{∃}), ¬P(y^{∀}).

Instantiation step:

P(y^{∀}), ¬P(y^{∀}).

The last step is not allowed in the above citations, so that another γ-step must be applied to the original formula in order to prove it. Our instantiation step, however, is perfectly sound: Since x^{∃} does not occur in ∀y: ¬P(y), the free variables x^{∃} and y^{∀} do not depend on each other and there is no reason to insist on x^{∃} being older than y^{∀}. Note that moving-in the existential quantifier transforms the original formula into the logically equivalent formula ∃x: P(x) ∨ ∀y: ¬P(y), which (after a preceding α-step) enables the δ-step introducing y^{∀} to come before the γ-step introducing x^{∃}.

Keeping small the variable-conditions generated by the δ-rule results in non-elementary reduction of the size of smallest proofs. This “liberalization of the δ-rule” has a history ranging from Smullyan (1968) over Hähnle & Schmitt (1994) to Baaz & Fermüller (1995). While the liberalized δ-rule of Smullyan (1968) is already able to prove the formula of Ex. 1.2 with a single γ-step, it is much more restrictive than the more liberalized δ-rule of Baaz & Fermüller (1995).

Note that liberalization of the δ-rule is not simple because it easily results in unsound calculi, cf. Kohlhase (1995) w.r.t. our Ex. 1.3 and Kohlhase (1998) w.r.t. our Ex. 5.18. The difficulty lies with instantiation steps that relate previously unrelated variables:

Example 1.3

∃x: ∀y: Q(x, y) ∨ ∃u: ∀v: ¬Q(v, u)

is not deductively valid (to wit, let Q be the identity relation on a non-trivial universe).

Consider the following proof attempt: One α-, two γ-, and two liberalized δ-steps result in

Q(x^{∃}, y^{∀}), ¬Q(v^{∀}, u^{∃}) (∗)

with variable-condition

R := {(x^{∃}, y^{∀}), (u^{∃}, v^{∀})}. (#)

(Note that the non-liberalized δ-rule would additionally have produced (x^{∃}, v^{∀}) or (u^{∃}, y^{∀}) or both, depending on the order of the proof steps.)

When we now instantiate x^{∃} with v^{∀}, we relate the previously unrelated variables u^{∃} and y^{∀}. Thus, our new goal

Q(v^{∀}, y^{∀}), ¬Q(v^{∀}, u^{∃})

must be equipped with the new variable-condition {(u^{∃}, y^{∀})}. Otherwise we could instantiate u^{∃} with y^{∀}, resulting in the tautology Q(v^{∀}, y^{∀}), ¬Q(v^{∀}, y^{∀}).

Note that in the standard framework of Skolemization and unification, this new variable-condition is automatically generated by the occur-check of unification: When we instantiate x^{∃} with v^{∀}(u^{∃}) in

Q(x^{∃}, y^{∀}(x^{∃})), ¬Q(v^{∀}(u^{∃}), u^{∃})

we get

Q(v^{∀}(u^{∃}), y^{∀}(v^{∀}(u^{∃}))), ¬Q(v^{∀}(u^{∃}), u^{∃}),

which cannot be reduced to a tautology because y^{∀}(v^{∀}(u^{∃})) and u^{∃} cannot be unified.

When we instantiate the variables x^{∃} and u^{∃} in the sequence (∗) in parallel via

σ := {x^{∃}↦v^{∀}, u^{∃}↦y^{∀}}, ($)

we have to check whether the newly imposed variable-conditions are consistent with the substitution itself. In particular, a cycle as given (for the R of (#)) by

y^{∀} σ^{−1} u^{∃} R v^{∀} σ^{−1} x^{∃} R y^{∀}

must not exist. Although this sounds fairly difficult, the formal treatment is quite simple.

2 Basic Notions, Notations, and Assumptions

We make use of “[…]” for stating two definitions, lemmas, or theorems (and their proofs etc.) in one, where the parts between ‘[’ and ‘]’ are optional and are meant to be all included or all omitted. ‘IN’ denotes the set of and ‘≺’ the ordering on natural numbers. We define IN_{+} := { n ∈ IN | 0 ≠ n }.

Let ‘R’ denote a binary relation. R is said to be a relation on A if dom(R) ∪ ran(R) ⊆ A. R is irreflexive if id ∩ R = ∅. It is A-reflexive if _{A}|id ⊆ R. Simply speaking of a reflexive relation we refer to the biggest A that is appropriate in the local context, and referring to this A we write R^{0} to ambiguously denote _{A}|id. Furthermore, we write R^{1} to denote R. For n ∈ IN_{+} we write R^{n+1} to denote R^{n}∘R, such that R^{n} denotes the n step relation for R. The transitive closure of R is R^{+} := ⋃_{n∈IN_{+}} R^{n}. The reflexive & transitive closure of R is R^{∗} := ⋃_{n∈IN} R^{n}. The reverse^{5} of R will be denoted with R^{−1}. R is terminating if there is no s: IN → dom(R) with s_{i} R s_{i+1} for all i ∈ IN.

Furthermore, we use ‘∅’ to denote the empty set as well as the empty function or empty word. By an (irreflexive) ordering ‘<’ (on A) we mean an irreflexive and transitive binary relation (on A), sometimes called “strict partial ordering” etc. by other authors. A reflexive ordering ‘≤’ on A is an A-reflexive, antisymmetric, and transitive relation on A. The reflexive ordering on A of an ordering < is (< ∪ id) ∩ (A×A). An ordering < is called wellfounded if > is terminating; where, as with all our asymmetric relation symbols, > := <^{−1}. The class of total functions from A to B is denoted with A → B. The class of (possibly) partial functions from A to B is denoted with A ⇝ B.

Validity is expected to be given with respect to some Σ-structure (Σ-algebra) A, assigning a universe (to each sort) and an appropriate function to each symbol in Σ. For X ⊆ V_{free} we denote the set of total A-valuations of X (i.e. functions mapping free variables to objects of the universe of A (respecting sorts)) with X → A and the set of (possibly) partial A-valuations of X with X ⇝ A. For π ∈ X → A we denote with ‘A⊎π’ the extension of A to the variables of X which are then treated as nullary constants. More precisely, we assume the existence of some evaluation function ‘eval’ such that eval(A⊎π) maps any term over Σ⊎X into the universe of A (respecting sorts) such that for all x ∈ X: eval(A⊎π)(x) = π(x). Moreover, eval(A⊎π) maps any formula B over Σ⊎X to TRUE or FALSE, such that B is valid in A⊎π iff eval(A⊎π)(B) = TRUE. We assume that the Substitution-Lemma holds in the sense that, for any substitution σ, Σ-structure A, and valuation π ∈ V_{free} → A, validity of a formula B in A ⊎ ((σ ⊎_{V_{free}\dom(σ)}|id) ∘ eval(A⊎π)) is logically equivalent to validity of Bσ in A⊎π. Finally, we assume that the value of the evaluation function on a term or formula B does not depend on the free variables that do not occur in B: eval(A⊎π)(B) = eval(A ⊎_{V_{free}(B)}|π)(B). Further properties of validity or evaluation are definitely not needed.

3 Two Versions of Variable-Conditions

In this section we formally describe two possible choices for the formal treatment of variable-conditions. The weak version works well with the non-liberalized δ-rule. The strong version is a little more difficult but can be used for the liberalized versions of the δ-rule. The presented material is rather formal, but this cannot be avoided and the following sections will be less difficult then.

Several binary relations on free variables will be introduced. The overall idea is that when (x, y) occurs in such a relation this means something like “x is older than y” or “the value of y depends on or is described in terms of x”.

Definition 3.1 (E_{σ}, U_{σ})

For a substitution σ with dom(σ) = V_{∃} we define the existential relation to be

E_{σ} := { (x′, x) | x′ ∈ V_{∃}(σ(x)) ∧ x ∈ V_{∃} }

and the universal relation to be

U_{σ} := { (y, x) | y ∈ V_{∀}(σ(x)) ∧ x ∈ V_{∃} }.

Definition 3.2 ([Strong] Existential R-Substitution) Let R be a variable-condition. σ is an existential R-substitution if σ is a substitution with dom(σ) = V_{∃} for which U_{σ} ∘ R is irreflexive. σ is a strong existential R-substitution if σ is a substitution with dom(σ) = V_{∃} for which (U_{σ} ∘ R)^{+} is a wellfounded ordering.

Note that, regarding syntax, (x^{∃}, y^{∀}) ∈ R is intended to mean that an existential R-sub-stitution σ may not replace x^{∃} with a term in which y^{∀} occurs, i.e. (y^{∀}, x^{∃}) ∈ U_{σ} must be disallowed, i.e. U_{σ}∘R must be irreflexive. Thus, the definition of a (weak) existential R-substitution is quite straightforward. The definition of a strong existential R-substi-tution requires an additional transitive closure because the strong version then admits a smaller R. To see this, take from Ex. 1.3 the variable-condition R of (#) and the σ of ($). As explained there, σ must not be a strong existential R-substitution due to the cycle y^{∀} U_{σ} u^{∃} R v^{∀} U_{σ} x^{∃} R y^{∀} which just contradicts the irreflexivity of (U_{σ}∘R)^{2}. Note that in practice w.l.o.g. U_{σ} and R can always be chosen to be finite, so that irreflexivity of (U_{σ}∘R)^{+} is then equivalent to (U_{σ}∘R)^{+} being a wellfounded ordering.

After application of a [strong] existential R-substitution σ, in case of (x^{∃}, y^{∀}) ∈ R, we have to ensure that x^{∃} is not replaced with y^{∀} via a future application of another [strong] existential R-substitution that replaces a free existential variable u^{∃} occurring in σ(x^{∃}) with y^{∀}. In this case, the new variable-condition has to contain (u^{∃}, y^{∀}). This means that E_{σ}∘R must be a subset of the updated variable-condition. For the weak version this is already enough. For the strong version we have to add an arbitrary number of steps with U_{σ}∘R again.

Definition 3.3 ([Strong] σ-Update)

Let R be a variable-condition and σ be an [strong] existential R-substitution.

The [strong] σ-update of R is E_{σ}∘R [ ∘ (U_{σ}∘R)^{∗}].

Example 3.4

In the proof attempt of Ex. 1.3 we applied the strong existential R-substitution

σ′ := {x^{∃}↦v^{∀}} ⊎_{V_{∃}\{x^{∃}}}|id

where R = {(x^{∃}, y^{∀}), (u^{∃}, v^{∀})}. Note that

U_{σ′} = {(v^{∀}, x^{∃})}

and

E_{σ′} =_{V_{∃}\{x^{∃}}}|id.

Thus:

\begin{aligned}E_{σ′}∘R ∘ (U_{σ′}∘R)^{0} & = & \{(u^{∃}, v^{∀})\} \\ E_{σ′}∘R ∘ (U_{σ′}∘R)^{1} & = & \{(u^{∃}, y^{∀})\} \\ E_{σ′}∘R ∘ (U_{σ′}∘R)^{2} & = & ∅ \end{aligned}

The strong σ′-update of R is then the new variable-condition {(u^{∃}, v^{∀}), (u^{∃}, y^{∀})}.

Let A be some Σ-structure. We now define a semantic counterpart of our existential Rsubstitutions, which we will call “existential (A, R)-valuation”. Suppose that e maps each free existential variable not directly to an object of A (of the same sort), but can additionally read the values of some free universal variables under an A-valuation π ∈ V_{∀} → A, i.e. e gets some π′ ∈ V_{∀} ⇝ A with π′⊆π as a second argument; short: e: V_{∃} → ((V_{∀} ⇝ A) → A). Moreover, for each free existential variable x, we require the set of read free universal variables (i.e. dom(π′)) to be identical for all π; i.e. there has to be some “semantic relation” S_{e} ⊆ V_{∀}×V_{∃} such that for all x ∈ V_{∃}:

e(x): (S_{e}⟨{x}⟩ → A) → A.

Note that, for each e, at most one semantic relation exists, namely

S_{e} := { (y, x) | y ∈ dom(⋃ (dom(e(x)))) ∧ x ∈ V_{∃} }.

Definition 3.5 (S_{e}, [Strong] Existential (A, R)-Valuation, ϵ)

Let R be a variable-condition, A a Σ-structure, and e: V_{∃} → ((V_{∀} ⇝ A) → A).

The semantic relation of e is S_{e} := { (y, x) | y ∈ dom(⋃ (dom(e(x)))) ∧ x ∈ V_{∃} }.

e is an existential (A, R)-valuation if S_{e} ∘ R is irreflexive and, for all x ∈ V_{∃}, e(x): (S_{e}⟨{x}⟩ → A) → A.

e is a strong existential (A, R)-valuation if (S_{e} ∘ R)^{+} is a wellfounded ordering and, for all x ∈ V_{∃},

e(x): (S_{e}⟨{x}⟩ → A) → A.

Finally, for applying [strong] existential (A, R)-valuations in a uniform manner, we define the function

ϵ: (V_{∃} → ((V_{∀} ⇝ A) → A)) → ((V_{∀} → A) → (V_{∃} → A))

by ( e ∈ V_{∃} → ((V_{∀} ⇝ A) → A), π ∈ V_{∀} → A, x ∈ V_{∃} )

ϵ(e)(π)(x) := e(x)(_{S_{e}⟨{x}⟩}|π).

Lemma 3.6 Let R be a variable-condition.

1. Let R′ be a variable-condition with R⊆R′.

For each [strong] existential (A, R′)-valuation e′ there is some

[strong] existential (A, R)-valuation e such that ϵ(e) = ϵ(e′).

2. Let σ be a [strong] existential R-substitution and R′ the [strong] σ-update of R. For each [strong] existential (A, R′)-valuation e′ there is some

[strong] existential (A, R)-valuation e such that for all π ∈ V_{∀} → A:

ϵ(e)(π) = σ ∘ eval(A ⊎ ϵ(e′)(π) ⊎ π).

4 The Weak Version

We are now going to define R-validity of a set of sequents with free variables, in terms of validity of a formula (where the free variables are treated as nullary constants).

Definition 4.1 (Validity)

Let R be a variable-condition, A a Σ-structure, and G a set of sequents.

G is R-valid in A if there is an existential (A, R)-valuation e such that G is (e, A)-valid.

G is (e, A)-valid if G is (π, e, A)-valid for all π ∈ V_{∀} → A.

G is (π, e, A)-valid if G is valid in A ⊎ ϵ(e)(π) ⊎ π.

G is valid in A if Γ is valid in A for all Γ ∈ G.

A sequent Γ is valid in A if there is some formula listed in Γ that is valid in A.

Validity in a class of Σ-structures is understood as validity in each of the Σ-structures of that class.

If we omit the reference to a special Σ-structure we mean validity (or reduction, cf. below) in some fixed class K of Σ-structures, e.g. the class of all Σ-structures (Σ-algebras) or the class of Herbrand Σ-structures (term-generated Σ-algebras), cf. Wirth& Gramlich (1994) for more interesting classes for establishing inductive validities.

Lemma 4.2 (Anti-Monotonicity of Validity in R) Let G be a set of sequents and R and R′ variable-conditions with R⊆R′. Now: If G is R′-valid in A, then G is R-valid in A.

Example 4.3 (Validity)

For x^{∃} ∈ V_{∃}, y^{∀} ∈ V_{∀}, the sequent x^{∃}=y^{∀} is ∅-valid in any A because we can choose S_{e} := V_{∀}×V_{∃} and e(x^{∃})(π) := π(y^{∀}) resulting in ϵ(e)(π)(x^{∃}) = e(x^{∃})(_{S_{e}⟨{x^{∃}}⟩}|π) = e(x^{∃})(_{V_{∀}}|π) = π(y^{∀}). This means that ∅-validity of x^{∃}=y^{∀} is the same as validity of ∀y: ∃x: x=y. Moreover, note that ϵ(e)(π) has access to the π-value of y^{∀} just as a raising function f for x in the raised (i.e. dually Skolemized) version f(y^{∀})=y^{∀} of ∀y: ∃x: x=y.

Contrary to this, for R := V_{∃}×V_{∀}, the same formula x^{∃}=y^{∀} is not R-valid in general because then the required irreflexivity of S_{e}∘R implies S_{e} = ∅, and e(x^{∃})(_{S_{e}⟨{x^{∃}}⟩}|π) = e(x^{∃})(_{∅}|π) = e(x^{∃})(∅) cannot depend on π(y^{∀}) anymore. This means that (V_{∃}×V_{∀})-validity of x^{∃}=y^{∀} is the same as validity of ∃x: ∀y: x=y. Moreover, note that ϵ(e)(π) has no access to the π-value of y^{∀} just as a raising function c for x in the raised version c=y^{∀} of ∃x: ∀y: x=y.

For a more general example let G = { A_{i,0} … A_{i,n_{i}−1} | i ∈ I }, where for i ∈ I and j ≺ n_{i} the A_{i,j} are formulas with free existential variables from x⃗ and free universal variables from y⃗. Then (V_{∃}×V_{∀})-validity of G means validity of ∃x⃗: ∀y⃗: ∀i ∈ I: ∃j ≺ n_{i}: A_{i,j}; whereas ∅-validity of G means validity of ∀y⃗: ∃x⃗: ∀i ∈ I: ∃j ≺ n_{i}: A_{i,j}.

Besides the notion of validity we need the notion of reduction. Roughly speaking, a set G_{0} of sequents reduces to a set G_{1} of sequents if validity of G_{1} implies validity of G_{0}. This, however, is too weak for our purposes here because we are not only interested in validity but also in preserving the solutions for the free existential variables: For inductive theorem proving, answer computation, and constraint solving it becomes important that the solutions of G_{1} are also solutions of G_{0}.

Definition 4.4 (Reduction)

G_{0} R-reduces to G_{1} in A if for all existential (A, R)-valuations e:

if G_{1} is (e, A)-valid then G_{0} is (e, A)-valid, too.

Lemma 4.5 (Reduction)

Let R, R′ be variable-conditions; A a Σ-structure; G_{0}, G_{1}, G_{2}, and G_{3} sets of sequents. Now:

1. (Validity)

If G_{0} R-reduces to G_{1} in A and G_{1} is R-valid in A,

then G_{0} is R-valid in A, too.

2. (Reflexivity)

In case of G_{0}⊆G_{1}: G_{0} R-reduces to G_{1} in A.

3. (Transitivity)

If G_{0} R-reduces to G_{1} in A and G_{1} R-reduces to G_{2} in A,

then G_{0} R-reduces to G_{2} in A.

4. (Additivity)

If G_{0} R-reduces to G_{2} in A and G_{1} R-reduces to G_{3} in A,

then G_{0}∪G_{1} R-reduces to G_{2}∪G_{3} in A.

5. (Monotonicity in R) In case of R⊆R′: If G_{0} R-reduces to G_{1} in A, then G_{0} R′-reduces to G_{1} in A.

6. (Instantiation)

For an existential R-substitution σ, and R′ the σ-update of R:

(a) If G_{0}σ is R′-valid in A, then G_{0} is R-valid in A.

(b) If G_{0} R-reduces to G_{1} in A, then G_{0}σ R′-reduces to G_{1}σ in A.

Now we are going to abstractly describe deductive sequent and tableau calculi. We will later show that the usual deductive first-order calculi are instances of our abstract calculi. The benefit of the abstract version is that every instance is automatically sound. Due to the small number of inference rules in deductive first-order calculi and the locality of soundness, this abstract version is not really necessary. For inductive calculi, however, due to a bigger number of inference rules (which usually have to be improved now and then) and the globality of soundness, such an abstract version is very helpful, cf. Wirth & Becker (1995), Wirth (1997).

Definition 4.6 (Proof Forest) A (deductive) proof forest in a sequent (or else: tableau) calculus is a pair (F, R) where R is a variable-condition and F is a set of pairs (Γ, t), where Γ is a sequent and t is a tree^{6} whose nodes are labeled with sequents (or else: formulas).

Note that the tree t is intended to represent a proof attempt for Γ. The nodes of t are labeled with formulas in case of a tableau calculus and with sequents in case of a sequent calculus. While the sequents at the nodes of a tree in a sequent calculus stand for themselves, in a tableau calculus all the ancestors have to be included to make up a sequent and, moreover, the formulas at the labels are in negated form:

Definition 4.7 (Goals(), AX, Closedness)

‘Goals(T)’ denotes the set of sequents labeling the leaves of the trees in the set T (or else: the set of sequents resulting from listing the conjugates of the formulas labeling a branch from a leaf to the root in a tree in T).

In what follows, we assume AX to be some set of axioms. By this we mean that AX is V_{∃}×V_{∀}-valid. (Cf. the last sentence in Def. 4.1.)

The tree t is closed if Goals({t}) ⊆ AX .

The readers may ask themselves why we consider a proof forest instead of a single proof tree only. The possibility to have an empty proof forest provides a nicer starting point. Besides that, if we have trees (Γ, t), (Γ′, t′) ∈ F we can apply Γ as a lemma in the tree t′ of Γ′, provided that the lemma application relation is acyclic. For deductive theorem proving the availability of lemma application is not really necessary. For inductive theorem proving, however, lemma and induction hypothesis application of this form becomes necessary.

Definition 4.8 (Invariant Condition) The invariant condition on (F, R) is that {Γ } R-reduces to Goals({t}) for all (Γ, t) ∈ F.

Theorem 4.9 Let the proof forest (F, R) satisfy the above invariant condition. Let (Γ, t) ∈ F. If t is closed, then Γ is R-valid.

Theorem 4.10

The above invariant condition is always satisfied when we start with an empty proof forest (F, R) := (∅, ∅) and then iterate only the following kinds of modifications of (F, R) (resulting in (F′, R′)):

Hypothesizing: Let R′ be a variable-condition with R⊆R′. Let Γ be a sequent. Let t be the tree with a single node only, which is labeled with Γ (or else: with a single branch only, such that Γ is the list of the conjugates of the formulas labeling the branch from the leaf to the root). Then we may set F′ := F ∪ {(Γ, t)}.

Expansion: Let (Γ, t) ∈ F. Let R′ be a variable-condition with R⊆R′. Let l be a leaf in t. Let Δ be the label of l (or else: result from listing the conjugates of the formulas labeling the branch from l to the root of t). Let G be a finite set of sequents. Now if {Δ} R′-reduces to G (or else: { ΛΔ | Λ ∈ G }), then we may set F′ := (F \{(Γ, t)})∪ {(Γ, t′)} where t′ results from t by adding to the former leaf l, exactly for each sequent Λ in G, a new child node labeled with Λ (or else: a new child branch such that Λ is the list of the conjugates of the formulas labeling the branch from the leaf to the new child node of l).

Instantiation: Let σ be an existential R-substitution. Let R′ be the σ-update of R. Then we may set F′ := F σ.

While Hypothesizing and Instantiation steps are self-explanatory, Expansion steps are parameterized by a sequent Δ and a set of sequents G such that {Δ} R′-reduces to G. For tableau calculi, however, this set of sequents must actually have the form { ΛΔ | Λ ∈ G } because an Expansion step cannot remove formulas from ancestor nodes. This is because these formulas are also part of the goals associated with other leaves in the proof tree. Therefore, although tableau calculi may save repetition of formulas, sequent calculi have substantial advantages: Rewriting of formulas in place is always possible, and we can remove formulas that are redundant w.r.t. the other formulas in a sequent. But this is not our subject here. For the below examples of α-, β-, γ-, and δ-rules we will use the sequent calculi presentation because it is a little more explicit. When we write

\frac{Δ}{Π_{0} … Π_{n−1}} R′′

we want to denote a sub-rule of the Expansion rule which is given by G := {Π_{0}, …, Π_{n−1}} and R′ := R ∪ R′′. This means that for this rule really being a sub-rule of the Expansion rule we have to show that {Δ} R′-reduces to G. By Lemma 4.5(5) and because R does not matter here, it suffices that we actually show that {Δ} R′′-reduces to G. Moreover, note that in old times when trees grew upwards, Gerhard Gentzen would have written Π_{0} … Π_{n−1} above the line and Δ below, such that passing the line meant implication. In our case, passing the line means reduction.

Let A and B be formulas, Γ and Π sequents, x ∈ V_{bound}, x^{∃} ∈ V_{∃} \ V_{∃}(A, Γ Π), ^{7} and x^{∀} ∈ V_{∀} \ V_{∀}(A, Γ Π).

α-rules:

\frac{Γ (A∨B) Π}{A B Γ Π} ∅

\frac{Γ ¬(A∧B) Π}{\overline{A} \overline{B} Γ Π} ∅

\frac{Γ ¬¬A Π}{A Γ Π} ∅

β-rules:

\frac{Γ (A∧B) Π}{A Γ Π  B Γ Π}  ∅

\frac{Γ ¬(A∨B) Π}{\overline{A} Γ Π  \overline{B} Γ Π}  ∅

γ-rules:

\frac{Γ ∃x: A Π}{A\{x↦x^{∃}\} Γ ∃x: A Π} ∅

\frac{Γ ¬∀x: A Π}{\overline{A\{x↦x^{∃}\}} Γ ¬∀x: A Π} ∅

δ-rules:

\frac{Γ ∀x: A Π}{A\{x↦x^{∀}\} Γ Π} V_{∃}(A, Γ Π) × \{x^{∀}\}

\frac{Γ ¬∃x: A Π}{\overline{A\{x↦x^{∀}\}} Γ Π} V_{∃}(A, Γ Π) × \{x^{∀}\}

Theorem 4.11 The above examples of α-, β-, γ-, and δ-rules are all sub-rules of the Expansion rule of the sequent calculus of Theor. 4.10.

5 The Strong Version

The additional solutions (or existential substitutions) of the strong version (which admit additional proofs compared to the weak version) do not add much difficulty when one is interested in validity only, cf. e.g. Hähnle & Schmitt (1994). When also the preservation of solutions is required, however, the additional substitutions pose some problems because the new solutions may tear some free universal variables out of their contexts:

Example 5.1 (Reduction & Liberalized δ-Steps)

In Ex. 1.2 a liberalized δ-step reduced

P(x^{∃}), ∀y: ¬P(y)

to

P(x^{∃}), ¬P(y^{∀})

with empty variable-condition R := ∅.

The latter sequent is (e, A)-valid for the strong existential (A, R)-valuation e given by e(x^{∃})(π) := π(y^{∀}).

The former sequent, however, is not (e, A)-valid when P^{A}(a) is true and P^{A}(b) is false for some a, b from the universe of A. To see this, take some π with π(y^{∀}) := b.

How can we solve the problem exhibited in Ex. 5.1? I.e. how can we change the notion of reduction such that the liberalized δ-step becomes a reduction step?

1. The approach we tried first was to allow a slight modification of e to e′ such that e′(x^{∃})(π) = a. This trial finally failed because it was not possible to preserve reduction under Instantiation-steps.

E.g., an Instantiation-step with the strong existential R-substitution {x^{∃}↦y^{∀}} transforms the reduction of Ex. 5.1 into the reduction of

P(y^{∀}), ∀y: ¬P(y)

to

P(y^{∀}), ¬P(y^{∀}).

Taking π, e, and A as in Ex. 5.1, the new latter sequent is still (e, A)-valid. There is, however, no modification e′ of e such that the new former sequent is (π, e′, A)-valid.

Thus, with this approach, reduction could not be preserved by Instantiation-steps.

Moreover, the modification of e does not go together well with our requirement of preservation of solutions.

2. Learning from this, the second approach we tried was to allow a slight modification of π instead. E.g., for the reduction step of Ex. 5.1, we would require the existence of some η ∈ {y^{∀}} → A such that the former sequent is (_{V_{∀}\{y^{∀}}}|π⊎η, e, A)-valid instead of (π, e, A)-valid. Choosing η := {y^{∀}↦a} would solve the problem of Ex. 5.1 then: Indeed, the former sequent is (_{V_{∀}\{y^{∀}}}|π⊎η, e, A)-valid because for the e of Ex. 5.1 we have e(x^{∃})(_{V_{∀}\{y^{∀}}}|π⊎η) = (_{V_{∀}\{y^{∀}}}|π⊎η)(y^{∀}) = a.

Moreover, with this approach, reduction is preserved under Instantiation-steps.

The problems with this approach arise, however, when one asks whether there has to be a single η for all π or, for each π, a different η.

If we require a single η, we cannot model liberalized δ-steps where another free universal variable, say z^{∀}, occurs in the principal formula, as, e.g., in the reduction of

z^{∀}=x^{∃}, ∀y: z^{∀}≠y

to

z^{∀}=x^{∃}, z^{∀}≠y^{∀}

with empty variable-condition. In this case, for the e of Ex. 5.1 (which gives x^{∃} the value of y^{∀}) the η ∈ {y^{∀}} → A must change when the π-value of z^{∀} changes: E.g., for π := {y^{∀}↦a, z^{∀}↦b} we need η(y^{∀}) := b, while for π := {y^{∀}↦b, z^{∀}↦a} we need η(y^{∀}) := a. Indeed, in the reduction above, y^{∀} is functionally dependent on z^{∀}.

If, on the other hand, we admit a different η for each π, the transitivity of reduction (cf. Lemma 4.5(3)) gets lost.

Thus, the only solution can be that η depends on some values of π and not on others. Since the abstract treatment of this gets very ugly and does not extract much information on the solution of free existential variables of the original theorem from a completed proof, we prefer to remember what role the free universal variables introduced by liberalized δ-steps really play. And this is what the following definition is about.

Definition 5.2 (Choice-Condition, Extension)

C is a (R, <)-choice-condition if C is a (possibly) partial function from V_{∀} into the set of formulas, R is a variable-condition, < is a wellfounded ordering on V_{∀} with (R ∘ <) ⊆ R, and, for all y^{∀} ∈ dom(C):

z^{∀} < y^{∀} for all z^{∀} ∈ V_{∀}(C(y^{∀}))\{y^{∀}}

and

u^{∃} R y^{∀} for all u^{∃} ∈ V_{∃}(C(y^{∀})).

(C′, R′, <′) is an extension of (C, R, <) if C⊆C′, R⊆R′, and C′ is a (R′, <′)-choice-condition.

Note that ∅ is a (R, ∅)-choice-condition for any variable-condition R. For the meaning of choice-conditions cf. Def. 5.6.

Definition 5.3 (Extended Strong σ-Update)

Let C be a (R, <)-choice-condition and σ a strong existential R-substitution.

The extended strong σ-update (C′, R′, <′) of (C, R, <) is given by C′ := { (x, Bσ) | (x, B) ∈ C }, R′ is the strong σ-update of R, <′ := < ∘ (U_{σ}∘R)^{∗} ∪ (U_{σ}∘R)^{+}.

Lemma 5.4 (Theorem 62 in Doornbos & al. (1997)) If A and B are two terminating relations with A∘B ⊆ A ∪ B∘(A ∪ B)^{∗}, then A ∪ B is terminating, too.

Lemma 5.5 (Extended Strong σ-Update) Let C be a (R, <)-choice-condition, σ a strong existential R-substitution, and (C′, R′, <′) the extended strong σ-update of (C, R, <). Now: C′ is a (R′, <′)-choice-condition.

Definition 5.6 (Compatibility) Let C be a (R, <)-choice-condition, A a Σ-structure, and e a strong existential (A, R)- valuation. We say that π is (e, A)-compatible with C if π ∈ V_{∀} → A and for each y^{∀} ∈ dom(C):

If C(y^{∀}) is (π, e, A)-valid,
then C(y^{∀}) is (_{V_{∀}\{y^{∀}}}|π ⊎ η, e, A)-valid for all η ∈ {y^{∀}} → A.

Note that (e, A)-compatibility of π with {(y^{∀}, B)} means that a different choice for the π-value of y^{∀} does not destroy the validity of the formula B in A ⊎ ϵ(e)(π) ⊎ π, or that π(y^{∀}) is chosen such that B becomes invalid if such a choice is possible, which is closely related to Hilbert’s ε-operator ( y^{∀} = εy: (¬B{y^{∀}↦y}) ).

We are now going to proceed like in the previous section, but using the strong versions instead of the weak ones.

Definition 5.7 (Strong Validity)

Let C be a (R, <)-choice-condition, A a Σ-structure, and G a set of sequents.

G is C-strongly R-valid in A if there is a strong existential (A, R)-valuation e such that G is C-strongly (e, A)-valid.

G is C-strongly (e, A)-valid if G is (π, e, A)-valid for each π that is (e, A)-compatible with C.

The rest is given by Def. 4.1.

Lemma 5.8 (Anti-Monotonicity in R and Monotonicity in C) Let G be a set of sequents, C a (R, <)-choice-condition, and C′ a (R′, <′)-choice-condition with R⊆R′ and C′⊆C. Now: If G is C′-strongly R′-valid in A, then G is C-strongly R-valid in A.

Example 5.9 (Strong Validity)

Note that ∅-validity does not differ from ∅-strong ∅-validity and that V_{∃}×V_{∀}-validity does not differ from ∅-strong V_{∃}×V_{∀}-validity. This is because the notions of weak and strong existential valuations do not differ in these cases. Therefore, Ex. 4.3 is also an example for strong validity.

Although ∅-strong R-validity always implies (weak) R-validity (because each strong existential (A, R)-valuation is a (weak) existential (A, R)-valuation), for R not being one of the extremes ∅ and V_{∃}×V_{∀}, (weak) R-validity and ∅-strong R-validity differ from each other. E.g. the sequent (∗) in Ex. 1.3 is (weakly) R-valid but not ∅-strongly R-valid for the R of (#): For S_{e} := {(y^{∀}, u^{∃}), (v^{∀}, x^{∃})} we get S_{e}∘R = {(y^{∀}, v^{∀}), (v^{∀}, y^{∀})}, which is irreflexive. Since the sequent (∗) is (e, A)-valid for the (weak) existential (A, R)-valuation e given by e(x^{∃})(_{S_{e}⟨{x^{∃}}⟩}|π) = π(v^{∀}) and e(u^{∃})(_{S_{e}⟨{u^{∃}}⟩}|π) = π(y^{∀}), the sequent (∗) is (weakly) R-valid in A. But (S_{e}∘R)^{2} is not irreflexive, so that this e is no strong existential (A, R)- valuation, which means that the sequent (∗) cannot be ∅-strongly R-valid in general.

For nonempty C, however, we must admit that C-strong R-validity is hard to understand. We have to make sure that C-strong R-validity can be easily understood in terms of ∅-strong R′-validity for some R′, which again implies (weak) R′-validity and ∅-validity. Note that this difficulty did not arise in the weak version because Lemma 4.2 states antimonotonicity of (weak) R-validity in R, whereas Lemma 5.8 states anti-monotonicity of C-strong R-validity in R but only monotonicity of C-strong R-validity in C.

Lemma 5.10 (Compatibility and Validity)

Let A be a Σ-structure, C a (R, <)-choice-condition, and e a strong existential (A, R)- valuation. Define ⊲ := (S_{e} ∪ R ∪ <)^{+}.

1. ⊲ is a wellfounded ordering on V_{free}.

2. There is a function ξ: ( (V_{∀}\dom(C)) → A ) → ( dom(C) → A ) such that, for all π, π′ ∈ (V_{∀}\dom(C)) → A, π ⊎ ξ_{π} is (e, A)-compatible with C, and, for x ∈ dom(C), _{⊲⟨{x}⟩}|π = _{⊲⟨{x}⟩}|π′ implies ξ_{π}(x) = ξ_{π′}(x).

3. Let G be a set of sequents and ς ∈ (V_{∀}(G) ∩ dom(C)) → (V_{∃}\V_{∃}(G)) be injective.

(a) If G is C-strongly (e, A)-valid, then Gς is ∅-strongly R′-valid in A

for R′ := _{V_{∃}\ran(ς)}|R ∪ ⋃_{y∈ran(ς)}{y} × ⟨{ς^{−1}(y)}⟩⊴ ∪ V_{∃} × dom(C),

where ⊴ is the reflexive ordering on V_{∀} of ⊲.

(b) If G is C-strongly R-valid in A, then Gς is ∅-strongly _{V_{∃}\ran(ς)}|R-valid in A and even ∅-strongly R′′-valid in A

for R′′ := _{V_{∃}\ran(ς)}|R ∪ ⋃_{y∈ran(ς)}{y} × ⟨{ς^{−1}(y)}⟩< ∪ V_{∃} × dom(C).

Definition 5.11 (Strong Reduction)

Let C be a (R, <)-choice-condition, A a Σ-structure, and G_{0}, G_{1} sets of sequents.

G_{0} strongly (R, C)-reduces to G_{1} in A if for each strong existential (A, R)-valuation e and each π that is (e, A)-compatible with C:

if G_{1} is (π, e, A)-valid, then G_{0} is (π, e, A)-valid.

Lemma 5.12 (Strong Reduction)

Let C be a (R, <)-choice-condition; A a Σ-structure; G_{0}, G_{1}, G_{2}, and G_{3} sets of sequents. Now:

1. (Validity)

Assume that G_{0} strongly (R, C)-reduces to G_{1} in A. Now:

If G_{1} is C-strongly (e, A)-valid for some strong existential (A, R)-valuation e, then G_{0} is C-strongly (e, A)-valid.

If G_{1} is C-strongly R-valid in A, then G_{0} is C-strongly R-valid in A.

2. (Reflexivity) In case of G_{0}⊆G_{1}: G_{0} strongly (R, C)-reduces to G_{1} in A.

3. (Transitivity) If G_{0} strongly (R, C)-reduces to G_{1} in A and G_{1} strongly (R, C)-reduces to G_{2} in A, then G_{0} strongly (R, C)-reduces to G_{2} in A.

4. (Additivity)

If G_{0} strongly (R, C)-reduces to G_{2} in A and G_{1} strongly (R, C)-reduces to G_{3} in A, then G_{0}∪G_{1} strongly (R, C)-reduces to G_{2}∪G_{3} in A.

5. (Monotonicity) For (C′, R′, <′) being an extension of (C, R, <): If G_{0} strongly (R, C)-reduces to G_{1} in A, then G_{0} strongly (R′, C′)-reduces to G_{1} in A.

6. (Instantiation)

For a strong existential R-substitution σ, and the extended strong σ-update (C′, R′, <′) of (C, R, <):

(a) If G_{0}σ is C′-strongly R′-valid in A, then G_{0} is C-strongly R-valid in A.

(b) If G_{0} strongly (R, C)-reduces to G_{1} in A, then G_{0}σ strongly (R′, C′)-reduces to G_{1}σ in A.

Now we are going to abstractly describe deductive sequent and tableau calculi. We will later show that the usual deductive first-order calculi are instances of our abstract calculi.

Definition 5.13 (Strong Proof Forest) A strong (deductive) proof forest in a sequent (or else: tableau) calculus is a quadruple (F, C, R, <) where C is a (R, <)-choice-condition and F is a set of pairs (Γ, t), where Γ is a sequent and t is a tree whose nodes are labeled with sequents (or else: formulas).

The notions of Goals(), AX, and closedness of Def. 4.7 are not changed. Note, however, that the V_{∃}×V_{∀}-validity of AX immediately implies the ∅-strong V_{∃}×V_{∀}-validity of AX, which (by Lemma 5.8) is the logically strongest kind of C-strong R-validity.

Definition 5.14 (Strong Invariant Condition) The strong invariant condition on (F, C, R, <) is that {Γ } strongly (R, C)-reduces to Goals({t}) for all (Γ, t) ∈ F.

Theorem 5.15 Let the strong proof forest (F, C, R, <) satisfy the above strong invariant condition. Let (Γ, t) ∈ F and t be closed. Now: Γ is C-strongly R-valid and, for any injective ς ∈ (V_{∀}(Γ) ∩ dom(C)) → (V_{∃}\V_{∃}(Γ)), Γ ς is ∅-strongly _{V_{∃}\ran(ς)}|R-valid and even ∅-strongly R′-valid for

R′ := _{V_{∃}\ran(ς)}|R ∪ ⋃_{y∈ran(ς)}{y} × ⟨{ς^{−1}(y)}⟩< ∪ V_{∃} × dom(C).

Theorem 5.16

The above strong invariant condition is always satisfied when we start with an empty strong proof forest (F, C, R, <) := (∅, ∅, ∅, ∅) and then iterate only the following kinds of modifications of (F, C, R, <) (resulting in (F′, C′, R′, <′)):

Hypothesizing: Let R′ := R∪R′′ be a variable-condition with (R′′∘<) ⊆ R′. Set C′ := C and <′ := <. Let Γ be a sequent. Let t be the tree with a single node only, which is labeled with Γ (or else: with a single branch only, such that Γ is the list of the conjugates of the formulas labeling the branch from the leaf to the root). Then we may set F′ := F ∪ {(Γ, t)}.

Expansion: Let (C′, R′, <′) be an extension of (C, R, <). Let (Γ, t) ∈ F. Let l be a leaf in t. Let Δ be the label of l (or else: result from listing the conjugates of the formulas labeling the branch from l to the root of t). Let G be a finite set of sequents. Now if {Δ} strongly (R′, C′)-reduces to G (or else: { ΛΔ | Λ ∈ G }), then we may set F′ := (F \{(Γ, t)}) ∪ {(Γ, t′)} where t′ results from t by adding to the former leaf l, exactly for each sequent Λ in G, a new child node labeled with Λ (or else: a new child branch such that Λ is the list of the conjugates of the formulas labeling the branch from the leaf to the new child node of l).

Instantiation: Let σ be a strong existential R-substitution. Let (C′, R′, <′) be the extended strong σ-update of (C, R, <). Then we may set F′ := F σ.

While Hypothesizing and Instantiation steps are self-explanatory, Expansion steps are parameterized by a sequent Δ and a set of sequents G such that {Δ} strongly (R′, C′)-reduces to G for some extension (C′, R′, <′) of (C, R, <). For the below examples of α-, β-, γ-, and δ-rules we will use the sequent calculi presentation because it is a little more explicit. When we write

\frac{Δ}{Π_{0} … Π_{n−1}}  \begin{matrix}C′′ \\ R′′ \\ <′′ \end{matrix}

we want to denote a sub-rule of the Expansion rule which is given by G := {Π_{0}, …, Π_{n−1}}, C′ := C ∪C′′, R′ := R ∪R′′, and <′ := <∪<′′. This means that for this rule really being a sub-rule of the Expansion rule we have to show that C′ is a (R′, <′)-choice-condition and that {Δ} strongly (R′, C′)-reduces to G.

Let A and B be formulas, Γ and Π sequents, x ∈ V_{bound}, x^{∃} ∈ V_{∃} \ V_{∃}(A, Γ Π), ^{8} and x^{∀} ∈ V_{∀} \ ( V_{∀}(A, Γ Π) ∪ dom(<) ∪ dom(C) ).

α-rules:

\frac{Γ (A∨B) Π}{A B Γ Π}  \begin{matrix}∅ \\ ∅ \\ ∅ \end{matrix}

\frac{Γ ¬(A∧B) Π}{\overline{A} \overline{B} Γ Π}  \begin{matrix}∅ \\ ∅ \\ ∅ \end{matrix}

\frac{Γ ¬¬A Π}{A Γ Π}  \begin{matrix}∅ \\ ∅ \\ ∅ \end{matrix}

β-rules:

\frac{Γ (A∧B) Π}{A Γ Π  B Γ Π}  \begin{matrix}∅ \\ ∅ \\ ∅ \end{matrix}

\frac{Γ ¬(A∨B) Π}{\overline{A} Γ Π  \overline{B} Γ Π}  \begin{matrix}∅ \\ ∅ \\ ∅ \end{matrix}

γ-rules:

\frac{Γ ∃x: A Π}{A\{x↦x^{∃}\} Γ ∃x: A Π}  \begin{matrix}∅ \\ ∅ \\ ∅ \end{matrix}

\frac{Γ ¬∀x: A Π}{\overline{A\{x↦x^{∃}\}} Γ ¬∀x: A Π}  \begin{matrix}∅ \\ ∅ \\ ∅ \end{matrix}

Liberalized δ-rules:

\frac{Γ ∀x: A Π}{A\{x↦x^{∀}\} Γ Π}  \begin{matrix}\{(x^{∀}, A\{x↦x^{∀}\})\} \\ (V_{∃}(A) ∪ R⟨V_{∀}(A)⟩) × \{x^{∀}\} \\ ≤⟨V_{∀}(A)⟩ × \{x^{∀}\} \end{matrix}

\frac{Γ ¬∃x: A Π}{\overline{A\{x↦x^{∀}\}} Γ Π}  \begin{matrix}\{(x^{∀}, \overline{A\{x↦x^{∀}\}})\} \\ (V_{∃}(A) ∪ R⟨V_{∀}(A)⟩) × \{x^{∀}\} \\ ≤⟨V_{∀}(A)⟩ × \{x^{∀}\} \end{matrix}

Theorem 5.17 The above examples of α-, β-, γ-, and liberalized δ-rules are all sub-rules of the Expansion rule of the sequent calculus of Theor. 5.16.

The following example shows that R′′ of the above liberalized δ-rule must indeed contain R⟨V_{∀}(A)⟩ × {x^{∀}}.

Example 5.18

∃y: ∀x: ( ¬Q(x, y) ∨ ∀z: Q(x, z) )

is not deductively valid (to wit, let Q be the identity relation on a non-trivial universe). γ-step:

∀x: ( ¬Q(x, y^{∃}) ∨ ∀z: Q(x, z) )

Liberalized δ-step:

( ¬Q(x^{∀}, y^{∃}) ∨ ∀z: Q(x^{∀}, z) )

with choice-condition (x^{∀}, (¬Q(x^{∀}, y^{∃}) ∨ ∀z: Q(x^{∀}, z))) and variable-condition (y^{∃}, x^{∀}). α-step:

¬Q(x^{∀}, y^{∃}), ∀z: Q(x^{∀}, z)

Liberalized δ-step:

¬Q(x^{∀}, y^{∃}), Q(x^{∀}, z^{∀})

with additional choice-condition (z^{∀}, Q(x^{∀}, z^{∀})) and additional variable-condition (y^{∃}, z^{∀}).

Note that the additional variable-condition arises although y^{∃} does not appear in Q(x^{∀}, z). The reason for the additional variable-condition is y^{∃} R x^{∀} ∈ V_{∀}(Q(x^{∀}, z)).

The variable-condition (y^{∃}, z^{∀}) is, however, essential for soundness, because without it we could complete the proof attempt by application of the strong existential {(y^{∃}, x^{∀})}- substitution σ := {y^{∃}↦z^{∀}} ⊎_{V_{∃}\{y^{∃}}}|id.

Another interesting point is that now that we have achieved our goal of liberalizing our δ-rule and strictly increasing our proving possibilities, we must not use our original nonliberalized δ-rule of Section 4 anymore. This sounds quite strange on the first view, but is simply due to our changed notion of reduction. More precisely,

Weak δ-rule:  \frac{Γ ∀x: A Π}{A\{x↦x^{∀}\} Γ Π}  \begin{matrix}∅ \\ (V_{∃}(A, Γ Π) ∪ R⟨V_{∀}(A, Γ Π)⟩) × \{x^{∀}\} \\ ≤⟨V_{∀}(A, Γ Π)⟩ × \{x^{∀}\} \end{matrix}

does not describe a sub-rule of the Expansion rule of the sequent calculus of Theor. 5.16. To see this, let us start with the empty proof tree (∅, ∅, ∅, ∅) and then hypothesize ∀x: x=0, which we abbreviate with Γ. Applying the above weak δ-rule we get x^{∀}=0 as the label of the only leaf in the tree t of the proof tree ((Γ, t), ∅, ∅, ∅). But, while {Γ } does ∅-reduce to {x^{∀}=0} (i.e. Goals({t})), {Γ } does not strongly (∅, ∅)-reduce to {x^{∀}=0}. To see this, consider some Σ-structure A with non-trivial universe, an arbitrary strong existential (A, ∅)-valuation e, and some π ∈ V_{∀} → A with π(x^{∀}) = 0^{A}. Then {x^{∀}=0} is (π, e, A)-valid, but {Γ } is not. If we had applied the liberalized δ-rule instead, we would have produced the proof tree ((Γ, t), C, ∅, ∅) with C = {(x^{∀}, x^{∀}=0)}. And, indeed, π is not (e, A)-compatible with C, and {Γ } does strongly (∅, C)-reduce to {x^{∀}=0}.

Note that there is a fundamental difference related to the occurrence of the universal quantification on π between the notion of (weak) reduction

… ( ∀π ∈ (V_{∀} → A): G_{1} (π, e, A)-valid ) ⇒ ( ∀π ∈ (V_{∀} → A): G_{0} (π, e, A)-valid ) …

and the notion of strong reduction

… ∀π ∈ (V_{∀} → A) …: ( G_{1} (π, e, A)-valid ⇒ G_{0} (π, e, A)-valid ) ….

This difference in the nature of reduction renders the weak version applicable in areas where the strong version is not. For this reason (and for the sake of stepwise presentation) we have included the weak version in this paper although the strong version will turn out to be superior in all aspects of the calculus of Theor. 5.17 treated in this paper.

This fundamental difference in the nature of reduction cannot be removed: Suppose to weaken the notion of strong reduction in the following definition: G_{0} quite-strongly (R, C)- reduces to G_{1} in A if for each strong existential (A, R)-valuation e: if G_{1} is C-strongly (e, A)-valid, then G_{0} is C-strongly (e, A)-valid. At first glance, this version seems to be very nice. One nice aspect is that quite-strong (R, ∅)-reduction is so similar to (weak) Rreduction that we could omit the weak version because it would be very unlikely to find an application of the weak version where the strong version would not be applicable. Another nice aspect is that with quite-strong reduction we could easily adapt our intended version of inductive theorem proving as described in Section 1.1, which is not so easy with strong reduction because the induction hypotheses application becomes difficult. But for the (really essential!) monotonicity of reduction as given in Lemma 5.12(5), quite-strong reduction produces the following two additional requirements: dom(C′\C) ∩ V_{∀}(G_{1} ∪ ran(C)) = ∅ and V_{∃}(G_{1}) × dom(C′\C) ⊆ R′. While the first requirement is unproblematic, the second one restricts the δ-rule even more, which is the opposite of our intention behind the strong version, namely to liberalize the δ-rule.

Moreover, note that (as far as Theor. 5.17 is concerned) the choice-conditions do not have any influence on our proofs and may be discarded. We could, however, use them for the following purposes:

1. We could use the choice-conditions in order to weaken our requirements for our set of axioms AX: Instead of ∅-strong V_{∃}×V_{∀}-validity of AX the weaker C-strong V_{∃}×V_{∀}- validity of AX is sufficient for Theor. 5.15.

2. If we add a functional behavior to a choice-condition C, i.e. if we require that for (x^{∀}, A) ∈ C the value for x^{∀} is not just an arbitrary one from the set of values that make A invalid, but a unique element of this set given by some choice-function, then we can use the choice-conditions for simulating the behavior of the δ^{+^{+}}-rule of Beckert & al. (1993) by using the same free universal variable for the same C-value and by later equating free universal variables whose C-values become equal during the proof.

3. Moreover, the choice-conditions may be used to get more interesting answers:

Example 5.19

Starting with the empty proof tree and hypothesizing

∀x: Q(x, x), ∃y: ( ¬Q(y, y) ∧ ¬P(y) ), P(z^{∃})

with the above rules we can produce a proof tree with the leaves

¬Q(y^{∃}, y^{∃}), Q(x^{∀}, x^{∀}), ∃y: ( ¬Q(y, y) ∧ ¬P(y) ), P(z^{∃})

and

¬P(y^{∃}), Q(x^{∀}, x^{∀}), ∃y: ( ¬Q(y, y) ∧ ¬P(y) ), P(z^{∃})

and the (∅, ∅)-choice-condition {(x^{∀}, Q(x^{∀}, x^{∀}))}.

The strong existential ∅-substitution {y^{∃}↦x^{∀}, z^{∃}↦x^{∀}} ⊎ _{V_{∃}\{y^{∃},z^{∃}}}|id closes the proof tree via an Instantiation step. The answer x^{∀} for our query variable z^{∃} is not very interesting unless we note that the choice-condition tells us to choose x^{∀} in such a way that Q(x^{∀}, x^{∀}) becomes false.

The rules of our weak version of Section 4 are not only unable to provide any information on free universal variables, but also unable to prove the hypothesized sequent, because they can only show

∀x: Q(x, x), ∃y: ( ¬Q(y, y) ∧ ¬P(y) ), ∃z: P(z)

instead.

Thus it is obvious that the calculus of Theor. 5.17 is not only superior to the calculus of Theor. 4.11 w.r.t. proving but also w.r.t. answer “computation”.

Finally, note that (concerning the calculus of Theor. 5.17) the ordering < is not needed at all when in the liberalized δ-steps we always choose a completely new free universal variable x^{∀} that does not occur elsewhere and when in the Hypothesizing steps we guarantee that ran(R′′) contains only new free universal variables that have not occurred before. The former is reasonable anyhow, because the free universal variables introduced by previous liberalized δ-steps cannot be used because they are in dom(C) and the use of a free universal variable from the input hypothesis deteriorates the result of our proof by giving this free universal variable an existential meaning (because it puts it into dom(C)) as explained in Theor. 5.15. The latter does not seem to be restrictive for any reasonable application.

All in all, when interested in proving only, the (compared to the weak version) additional choice-condition and ordering of the strong version do not produce any overhead because they can simply be omitted. This is interesting because choice-conditions or Hilbert’s εexpressions are sometimes considered to make proofs quite complicated. When interested in answer “computation”, however, they could turn out to be useful.

W.r.t. the calculus of Theor. 5.17 we thus may conclude that the strong version is generally better than the weak version and the only overhead seems to be that we have to compute transitive closures when checking whether a substitution σ is really a strong existential Rsubstitution and when computing the strong σ-update of R. But we actually do not have to compute the transitive closure at all, because the only essential thing is the circularity-check which can be done on a bipartite^{9} graph generating the transitive closures. This checking is in the worst case linear in

|R| + ∑_{σ} ( |U_{σ}| + |E_{σ}| )

and is expected to perform at least as well as an optimally integrated version (i.e. one without conversion of term-representation) of the linear unification algorithm of Paterson & Wegman (1978) in the standard framework of Skolemization and unification. Note, however, that the checking for strong existential R-substitutions can also be implemented with any other unification algorithm.

Not really computing the transitive closure enables another refinement that allows us to go even beyond the fascinating strong Skolemization of Nonnengart (1996). The basic idea of Nonnengart (1996) can be translated into our framework in the following simplified way.

Instead of proving ∀x: (A∨B) it may be advantageous to prove the stronger ∀x: A ∨ ∀x: B, because after applications of α- and liberalized δ-rules to ∀x: A ∨ ∀x: B, resulting in A{x↦xA^{∀}}, B{x↦xB^{∀}}, the variable-conditions introduced for xA^{∀} and xB^{∀} may be smaller than the variable-condition introduced for y^{∀} after applying these rules to

∀x: (A∨B), resulting in A{x↦y^{∀}}, B{x↦y^{∀}}, i.e. R⟨{xA^{∀}}⟩ and R⟨{xB^{∀}}⟩ may be proper

subsets of R⟨{y^{∀}}⟩. Therefore the proof of ∀x: A ∨ ∀x: B may be simpler than the proof of ∀x: (A∨B). The nice aspect of Nonnengart (1996) is that the proofs of ∀x: A and ∀x: (A∨B) can be done in parallel without extra costs, such that the bigger variable-con-dition becomes active only if we decide that the smaller variable-condition is not enough to prove ∀x: A and we had better prove the weaker ∀x: (A∨B).

The disadvantage of the strong Skolemization approach of Nonnengart (1996), however, is that we have to decide whether to prove either ∀x: A or else ∀x: B in parallel to ∀x: (A∨B). In terms of Hilbert’s ε-operator, this asymmetry can be understood from the argumentation of Nonnengart (1996), which, for some new variable z ∈ V_{bound} and t denoting the term εz: (¬A{x↦z} ∧ (A ∨ x=z)), employs the logical equivalence of ∀x: (A∨B) with ∀x: A ∨ ∀x: (B{x↦t}) and then the logical equivalence of ∀x: A with ∃x: (A{x↦t}).

Now, if we do not really compute the transitive closures in our strong version, we can prove A{x↦xA^{∀}}, B{x↦xB^{∀}} in parallel and may later decide to prove the stronger A{x↦y^{∀}}, B{x↦y^{∀}} instead, simply by merging the nodes for xA^{∀} and xB^{∀} and substituting

xA^{∀} and xB^{∀} with y^{∀}.

6 Conclusion

All in all, we have presented an easy to read combination of raising, explicit variable dependency representation, the liberalized δ-rule, and preservation of solutions for first-order deductive theorem proving. Our motivation was not only to make these subjects more popular, but also to provide the foundation for our work on inductive theorem proving (cf. Wirth (1999)) where the preservation of solutions is indispensable.

To our knowledge^{10} we have presented on the one hand the first sound combination of explicit variable dependency representation and the liberalized δ-rule and on the other hand the first framework for preservation of solutions in full first-order logic.

Finally, the described problems with the development of the strong version reveal unexpected details on the nature of the liberalized δ-rule, and the discussion at the end of Section 5 opens up several new research directions.

7 The Proofs

Proof of Lemma 3.6

(1): Since e′ is a [strong] existential (A, R′)-valuation, S_{e′}∘R′ [ ∘ (S_{e′}∘R′)^{∗}] is irreflexive [and a wellfounded ordering]. Since R⊆R′, we have S_{e′}∘R [ ∘ (S_{e′}∘R)^{∗}] ⊆ S_{e′}∘R′ [ ∘ (S_{e′}∘R′)^{∗}]. Thus S_{e′}∘R [ ∘ (S_{e′}∘R)^{∗}] is irreflexive [and a wellfounded ordering], too. Therefore, setting e := e′, we get a [strong] existential (A, R)-valuation trivially satisfying the requirements.

(2): Here we denote concatenation (product) of relations ‘∘’ simply by juxtaposition and assume it to have higher priority than any other binary operator. Let e′ be some [strong] existential (A, R′)-valuation. Define S_{e} := S_{e′}E_{σ} ∪ U_{σ} and the [strong] existential (A, R)- valuation e by (x ∈ V_{∃}, π′ ∈ S_{e}⟨{x}⟩ → A):

e(x)(π′) := eval(A ⊎ ϵ(e′)(π) ⊎ π)(σ(x))

where π ∈ V_{∀} → A is an arbitrary extension of π′. For this definition to be okay, we have to prove the following claims: \underline{Claim 1:} For y ∈ V_{∀}(σ(x)), the choice of π ⊇ π′ does not influence the value of π(y). \underline{Claim 2:} For x′ ∈ V_{∃}(σ(x)), the choice of π ⊇ π′ does not influence the value of ϵ(e′)(π)(x′). \underline{Claim 3:} For the weak version we have to show that S_{e}R is irreflexive. \underline{Claim 4:} For the strong version we have to show that (S_{e}R)^{+} is a wellfounded ordering. \underline{Proof of Claim 1:} y ∈ V_{∀}(σ(x)) means (y, x) ∈ U_{σ}. By definition of S_{e} we have (y, x) ∈ S_{e}, i.e. y ∈ S_{e}⟨\{x\}⟩ = dom(π′). \underline{Q.e.d. (Claim 1)} \underline{Proof of Claim 2:} x′ ∈ V_{∃}(σ(x)) means (x′, x) ∈ E_{σ}. Thus by definition of S_{e} we have S_{e′}{(x′, x)} ⊆ S_{e}, i.e. S_{e′}⟨{x′}⟩ ⊆ S_{e}⟨{x}⟩ = dom(π′). Therefore ϵ(e′)(π)(x′) = e′(x′)(_{S_{e′}⟨\{x′\}⟩}|π) = e′(x′)(_{S_{e′}⟨\{x′\}⟩}|π′). \underline{Q.e.d. (Claim 2)} \underline{Proof of Claim 3:} Since S_{e}R = S_{e′}E_{σ}R ∪ U_{σ}R and U_{σ}R is irreflexive (as σ is an existential R-substitution), it suffices to show irreflexivity of S_{e′}E_{σ}R. Since R′ is the σ-update of R, this is equal to S_{e′}R′, which is irreflexive because e′ is an existential (A, R′)-valuation. Q.e.d. (Claim 3) \underline{Proof of Claim 4:} Since σ is a strong existential R-substitution, (U_{σ}R)^{+} is a wellfounded ordering. Thus, if (S_{e}R)^{+} = (S_{e′}E_{σ}R ∪ U_{σ}R)^{+} = (U_{σ}R)^{+} ∪ (U_{σ}R)^{∗}(S_{e′}E_{σ}R(U_{σ}R)^{∗})^{+} is not a wellfounded ordering, there must be an infinite descending sequence of the form y_{2i+2} (U_{σ}R)^{∗} y_{2i+1} (S_{e′}E_{σ}R(U_{σ}R)^{∗})^{+} y_{2i} for all i ∈ IN. But then y_{2i+3} (S_{e′}E_{σ}R(U_{σ}R)^{∗})^{+} y_{2i+2} (U_{σ}R)^{∗} y_{2i+1}, which contradicts the wellfoundedness of (S_{e′}E_{σ}R(U_{σ}R)^{∗})^{+}(U_{σ}R)^{∗} = (S_{e′}E_{σ}R(U_{σ}R)^{∗})^{+} = (S_{e′}R′)^{+}, where the latter step is due to R′ being the strong σ-update of R. The latter relation is a wellfounded ordering, however, because e′ is a strong existential (A, R′)-valuation. Q.e.d. (Claim 4)

Now, for π ∈ V_{∀} → A and x ∈ V_{∃} we have

ϵ(e)(π)(x) = e(x)(_{S_{e}⟨{x}⟩}|π) = eval(A ⊎ ϵ(e′)(π) ⊎ π)(σ(x))

i.e. ϵ(e)(π) = σ ∘ eval(A ⊎ ϵ(e′)(π) ⊎ π).

Q.e.d. (Lemma 3.6)

Proof of Lemma 4.2 This a trivial consequence of Lemma 3.6(1). Q.e.d. (Lemma 4.2)

Proof of Lemma 4.5 (1), (2), (3), and (4) are trivial. Note that (5) is a trivial consequence of Lemma 3.6(1).

\underline{(6a):} Suppose that G_{0}σ is R′-valid in A. Then there is some existential (A, R′)-valuation e′ such that G_{0}σ is (e′, A)-valid. Then, by Lemma 3.6(2), there is some existential (A, R)- valuation e such that for all π ∈ V_{∀} → A: ϵ(e)(π) = σ ∘ eval(A ⊎ ϵ(e′)(π) ⊎ π). Moreover, for y ∈ V_{∀} we have: π(y) = eval(A ⊎ ϵ(e′)(π) ⊎ π)(y), i.e. ϵ(e)(π) ⊎ π = (σ ⊎_{V_{∀}}|id) ∘ eval(A ⊎ ϵ(e′)(π) ⊎ π). Thus, for any formula B, we have

eval(A ⊎ ϵ(e)(π) ⊎ π)(B)  =
eval(A ⊎ ((σ ⊎_{V_{∀}}|id) ∘ eval(A ⊎ ϵ(e′)(π) ⊎ π)))(B) =
eval(A ⊎ ϵ(e′)(π) ⊎ π)(Bσ),

the latter step being due to the Substitution-Lemma.

Thus, for any set of sequents G′:

(e, A)-validity of G′ is logically equivalent to (e′, A)-validity of G′σ . (:§)

Especially, G_{0} is (e, A)-valid. Thus, G_{0} is R-valid in A.

\underline{(6b):} Let e′ be some existential (A, R′)-valuation and suppose that G_{1}σ is (e′, A)-valid. Let e be the existential (A, R)-valuation given by Lemma 3.6(2). Then, by (§) in the proof of (6a), G_{1} is (e, A)-valid. By assumption, G_{0} R-reduces to G_{1}. Thus, G_{0} is (e, A)-valid. By (§) in the proof of (6a), this means that G_{0}σ is (e′, A)-valid. Q.e.d. (Lemma 4.5)

Proof of Theor. 4.9 Since AX is V_{∃}×V_{∀}-valid, t is closed, and R ⊆ V_{∃}×V_{∀}, by Lemma 4.5(5), Goals({t}) is R-valid. Since (Γ, t) ∈ F and (F, R) satisfies the invariant condition, {Γ } R-reduces to Goals({t}). All in all, by Lemma 4.5(1), Γ is R-valid. Q.e.d. (Theor. 4.9)

Proof of Theor. 4.10 (∅, ∅) trivially satisfies the invariant condition. For the iteration steps, let (Γ′′, t′′) ∈ F′. Assuming the invariant condition for (F, R), we have to show that {Γ′′} R′-reduces to Goals({t′′}).

\underline{Hypothesizing:} In case of (Γ′′, t′′) ∈ F, \{Γ′′\} R-reduces to Goals(\{t′′\}) by assumption, and then, due to R⊆R′ and Lemma 4.5(5), {Γ′′} R′-reduces to Goals({t′′}). Otherwise we have (Γ′′, t′′) = (Γ, t). Then {Γ′′} = {Γ } = Goals({t}) = Goals({t′′}). Thus, by Lemma 4.5(2), {Γ′′} R′-reduces to Goals({t′′}).

\underline{Expansion:} In case of (Γ′′, t′′) ∈ F, \{Γ′′\} R-reduces to Goals(\{t′′\}) by assumption, and then, due to R⊆R′ and Lemma 4.5(5), {Γ′′} R′-reduces to Goals({t′′}). Otherwise we have (Γ′′, t′′) = (Γ, t′). Since Goals({t})\{Δ} ⊆ Goals({t′}), by Lemma 4.5(2), Goals({t})\{Δ} R′-reduces to Goals({t′}). Thus, since by assumption {Δ} R′-reduces to a subset of Goals({t′}), by Lemma 4.5(4) Goals({t}) R′-reduces to Goals({t′}). Moreover, due to (Γ, t) ∈ F, by assumption {Γ } R-reduces to Goals({t}). Thus, by R⊆R′ and Lemma 4.5(5), {Γ } R′-reduces to Goals({t}). Thus, since Goals({t}) R′-reduces to Goals({t′}), by Lemma 4.5(3) {Γ } R′-reduces to Goals({t′}), i.e. {Γ′′} R′-reduces to Goals({t′′}).

\underline{Instantiation:} There is some (Γ, t) ∈ F such that (Γ, t)σ = (Γ′′, t′′). By assumption, \{Γ \} R-reduces to Goals({t}). By Lemma 4.5(6), {Γ σ} R′-reduces to Goals({t})σ, i.e. {Γ′′} R′-reduces to Goals({t′′}). Q.e.d. (Theor. 4.10)

Proof of Theor. 4.11

Let A be an arbitrary Σ-structure (Σ-algebra). We only prove the first example of each kind of rule to be a sub-rule of the Expansion rule and leave the rest as an exercise.

\underline{α-rule:} We have to show that \{Γ (A∨B) Π\} ∅-reduces to \{A B Γ Π\} in A. This is trivial, however, because (e, A)-validity of the two sets is logically equivalent for each existential (A, ∅)-valuation e.

\underline{β-rule:} We have to show that \{Γ (A∧B) Π\} ∅-reduces to \{A Γ Π, B Γ Π\} in A. This is trivial, however, because (e, A)-validity of the two sets is logically equivalent for each existential (A, ∅)-valuation e.

\underline{γ-rule:} We have to show that \{Γ ∃x: A Π\} ∅-reduces to \{A\{x↦x^{∃}\} Γ ∃x: A Π\} in A. This is the case, however, because (e, A)-validity of the two sets is logically equivalent for each existential (A, ∅)-valuation e. The direction from left to right is given because the former sequent is a sub-sequent of the latter. The other direction, which is the only one we actually have to show here, is also clear because (π, e, A)-validity of A{x↦x^{∃}} implies (π, e, A)-validity of ∃x: A. Although this is clear, we should be a little more explicit here because the standard semantic definition of ∃ (cf. e.g. Wirth (1997), p. 188) does not use free existential variables and is somewhat more complicated than it could be in terms of free existential variables. Moreover, in the note above the theorem we remarked that the restriction on x^{∃} not occurring in the former sequent is not really necessary. Thus, in order to be more explicit here, assume that the latter sequent is (e, A)-valid for some existential (A, ∅)-valuation e. Let π ∈ V_{∀} → A. We have to show that the former sequent is (π, e, A)- valid. If this is not the case, A{x↦x^{∃}} must be (π, e, A)-valid. Let y^{∀} ∈ V_{∀}\V_{∀}(A). Then, since A{x↦y^{∀}}{y^{∀}↦x^{∃}} is equal to A{x↦x^{∃}}, we know that A{x↦y^{∀}}{y^{∀}↦x^{∃}} is valid in A⊎ϵ(e)(π)⊎π. Then, by the Substitution-Lemma, A{x↦y^{∀}} is valid in A⊎ϵ(e)(π)⊎π′ for π′ ∈ V_{∀} → A given by _{V_{∀}\{y^{∀}}}|π′ := _{V_{∀}\{y^{∀}}}|π and π′(y^{∀}) := ϵ(e)(π)(x^{∃}). By the standard semantic definition of ∃ and since quantification on x cannot occur in A (as ∃x: A is a formula in our restricted sense, cf. Section 1.4), this means that ∃x:(A{x↦y^{∀}}{y^{∀}↦x}) is valid in A ⊎ ϵ(e)(π) ⊎ π. Since y^{∀} does not occur in A, this formula is equal to ∃x:A, which means that the former sequent is (π, e, A)-valid as was to be shown.

\underline{δ-rule:} We have to show that \{Γ ∀x: A Π\} R′′-reduces to \{A\{x↦x^{∀}\} Γ Π\} in A for R′′ = V_{∃}(A, Γ Π) × {x^{∀}}. Assume that the latter sequent is (e, A)-valid for some existential R′′-valuation e. Let π ∈ V_{∀} → A. We have to show that the former sequent is (π, e, A)- valid. If some formula in Γ Π is (π, e, A)-valid, then the former sequent is (π, e, A)-valid, too. Otherwise, Γ Π is not only invalid in A⊎ϵ(e)(π)⊎π, but also in A⊎ϵ(e)(π)⊎π′ for all π′ ∈ V_{∀} → A with _{V_{∀}\{x^{∀}}}|π′ = _{V_{∀}\{x^{∀}}}|π, simply because x^{∀} does not occur in Γ Π. Because of V_{∃}(Γ Π) × {x^{∀}} ⊆ R′′, we know that Γ Π must be even invalid in A⊎ϵ(e)(π′)⊎π′. Since the latter sequent is assumed to be (e, A)-valid, this means that A{x↦x^{∀}} is (π′, e, A)-valid. Because of V_{∃}(A{x↦x^{∀}}) × {x^{∀}} = V_{∃}(A) × {x^{∀}} ⊆ R′′, we know that A{x↦x^{∀}} must be even valid in A ⊎ ϵ(e)(π) ⊎ π′ for all π′ ∈ V_{∀} → A with _{V_{∀}\{x^{∀}}}|π′ = _{V_{∀}\{x^{∀}}}|π. By the standard semantic definition of ∀ (cf. e.g. Wirth (1997), p. 188) and since quantification on x cannot occur in A (as ∀x: A is a formula in our restricted sense, cf. Section 1.4), this means that ∀x:(A{x↦x^{∀}}{x^{∀}↦x}) is valid in A ⊎ ϵ(e)(π) ⊎ π. Since x^{∀} does not occur in A, this formula is equal to ∀x:A, which means that the former sequent is (π, e, A)-valid as was to be shown.

Q.e.d. (Theor. 4.11)

Proof of Lemma 5.4

Since in Doornbos & al. (1997) Theorem 62 and especially its proof (which is used to illustrate the application of the very special framework of that paper) are not easy to read, we give an easier proof here that requires fewer set theoretical preconditions and uses induction only on ω. It proceeds by showing the existence of a refutational element in a nonempty set of infinite descending sequences.

Set F := dom(A) ∪ ran(A) ∪ dom(B) ∪ ran(B). We show that C := { t: IN → F | ∀i ∈ IN: t_{i} (A∪B) t_{i+1} } is empty. Otherwise we can choose s ∈ C and families (D_{i})_{i∈IN} and (E_{i})_{i∈IN_{+}} of subsets of F inductively in the following way: D_{0} := { t_{0} | t ∈ C }. Choose s_{0} such that it is B-irreducible in D_{0}, i.e. such that s_{0} ∈ D_{0} and there is no t′ ∈ D_{0} such that s_{0} B t′. For n ∈ IN_{+}: D_{n} := { t_{n} | t ∈ C ∧ ∀i ≺ n: t_{i} = s_{i} ∧ s_{n−1} A t_{n} }. E_{n} := { t_{n} | t ∈ C ∧ ∀i ≺ n: t_{i} = s_{i} ∧ s_{n−1} B t_{n} }. If E_{n} is nonempty we choose s_{n} from E_{n}. Otherwise, we choose s_{n} to be B-irreducible in D_{n}.

Since s ∈ C and A is terminating, there is some minimal n ∈ IN with s_{n} B s_{n+1}. We have n ≻ 0, because otherwise s_{0} B s_{1} ∈ D_{0} contradicts the choice of s_{0}. Thus, s_{n−1} (A\B) s_{n} B s_{n+1}. Since s_{n−1} (A\B) s_{n}, we know that s_{n} was chosen not from E_{n}, but B-irreducible in D_{n}. Due to A∘B ⊆ A ∪ B∘(A ∪ B)^{∗} we get two possible cases now.

\underline{s_{n−1} A s_{n+1}:} Then s_{0} … s_{n−1}s_{n+1}s_{n+2} … is an element of C. Thus, s_{n+1} ∈ D_{n}. Due to s_{n} B s_{n+1}, this contradicts s_{n} being B-irreducible in D_{n}.

\underline{s_{n−1} (B∘(A ∪ B)^{∗}) s_{n+1}:} Then there are some m ∈ IN and some s_{0} … s_{n−1}u_{0} … u_{m}s_{n+2}s_{n+3} … in C with s_{n−1} B u_{0} and u_{m} = s_{n+1} . Thus, u_{0} ∈ E_{n}, i.e. E_{n} is not empty. But this contradicts the fact that s_{n} was not chosen from E_{n}.

Q.e.d. (Lemma 5.4)

Proof of Lemma 5.5

Here we denote concatenation (product) of relations ‘∘’ simply by juxtaposition and assume it to have higher priority than any other binary operator.

\underline{Claim 1:} R′<′ ⊆ R′. \underline{Proof of Claim 1:} Since C is a (R, <)-choice-condition, we have R< ⊆ R. Thus, R′<′ = E_{σ}R(U_{σ}R)^{∗}(<(U_{σ}R)^{∗} ∪ (U_{σ}R)^{+}) = E_{σ}(RU_{σ})^{∗}R<(U_{σ}R)^{∗} ∪ E_{σ}R(U_{σ}R)^{∗}(U_{σ}R)^{+} ⊆ E_{σ}(RU_{σ})^{∗}R(U_{σ}R)^{∗} ∪ E_{σ}R(U_{σ}R)^{∗}(U_{σ}R)^{+} = E_{σ}R(U_{σ}R)^{∗}(U_{σ}R)^{∗} ∪ E_{σ}R(U_{σ}R)^{+} = E_{σ}R(U_{σ}R)^{∗} = R′. \underline{Q.e.d. (Claim 1)} \underline{Claim 2:} <′ is a wellfounded ordering on V_{∀}. \underline{Proof of Claim 2:} Since C is a (R, <)-choice-condition, we know that < is a wellfounded ordering on V_{∀} and R< ⊆ R. Thus U_{σ}R< ⊆ U_{σ}R,

(U_{σ}R)^{+}< = (U_{σ}R)^{∗}U_{σ}R< ⊆ (U_{σ}R)^{∗}U_{σ}R = (U_{σ}R)^{+},

and <(U_{σ}R)^{∗}< = << ∪ <(U_{σ}R)^{+}< ⊆ < ∪ <(U_{σ}R)^{+} = <(U_{σ}R)^{∗}. Since σ is a strong existential R-substitution, we know that (U_{σ}R)^{+} is a is a wellfounded ordering on V_{∀}. By Lemma 5.4 (setting A := <^{−1} and B := (U_{σ}R)^{−1}) by the first of the above containments, we know that <^{−1} ∪ (U_{σ}R)^{−1} is terminating, which (due to <′ = <(U_{σ}R)^{∗} ∪ (U_{σ}R)^{+} ) means that >′ is terminating, too. Finally <′ is also transitive, since by the above containments:

<(U_{σ}R)^{∗}<(U_{σ}R)^{∗} ⊆ <(U_{σ}R)^{∗}(U_{σ}R)^{∗} = <(U_{σ}R)^{∗} ⊆ <′

and <(U_{σ}R)^{∗}(U_{σ}R)^{+} = <(U_{σ}R)^{+} ⊆ <(U_{σ}R)^{∗} ⊆ <′ and (U_{σ}R)^{+}<(U_{σ}R)^{∗} ⊆ (U_{σ}R)^{+}(U_{σ}R)^{∗} = (U_{σ}R)^{+} ⊆ <′

and  (U_{σ}R)^{+}(U_{σ}R)^{+} ⊆ (U_{σ}R)^{+} ⊆ <′.  \underline{Q.e.d. (Claim 2)}

\underline{Claim 3:} For all y^{∀} ∈ dom(C′): For all z^{∀} ∈ V_{∀}(C′(y^{∀}))\\{y^{∀}\}: z^{∀} <′ y^{∀}. \underline{Proof of Claim 3:} Let z^{∀} ∈ V_{∀}(C′(y^{∀}))\\{y^{∀}\}. By the definition of C′ this means z^{∀} ∈ V_{∀}(C(y^{∀}))\{y^{∀}} or there is some u^{∃} ∈ V_{∃}(C(y^{∀})) with z^{∀} U_{σ} u^{∃}. Since C is a (R, <)- choice-condition, we have z^{∀} < y^{∀} or z^{∀} U_{σ} u^{∃} R y^{∀}. Thus, by definition of <′ we have z^{∀} <′ y^{∀}. \underline{Q.e.d. (Claim 3)}

\underline{Claim 4:} For all y^{∀} ∈ dom(C′): For all u^{∃} ∈ V_{∃}(C′(y^{∀})): u^{∃} R′ y^{∀}. \underline{Proof of Claim 4:} Let u^{∃} ∈ V_{∀}(C′(y^{∀})). By the definition of C′ there is some v^{∃} ∈ V_{∃}(C(y^{∀})) with u^{∃} E_{σ} v^{∃}. Since C is a (R, <)-choice-condition, we have v^{∃} R y^{∀}. Thus, by definition of R′ we have u^{∃} R′ y^{∀}. \underline{Q.e.d. (Claim 4)}

Q.e.d. (Lemma 5.5)

Proof of Lemma 5.8 Since G is C′-strongly R′-valid in A, there is some strong existential (A, R′)-valuation e′ such that G is C′-strongly (e′, A)-valid. Let e be the strong existential (A, R)-valuation with ϵ(e) = ϵ(e′) given by Lemma 3.6(1) due to R⊆R′. Let π be (e, A)-compatible with C. It suffices to show that G is (π, e, A)-valid. Since the notion of (e, A)-compatibility does not depend on the precise form of e besides ϵ(e), we know that π is also (e′, A)-compatible with C. Due to C′⊆C, π is also (e′, A)-compatible with C′. Finally, since G is C′-strongly (e′, A)-valid, we conclude that G is (π, e′, A)-valid, i.e. (π, e, A)-valid. Q.e.d. (Lemma 5.8)

Proof of Lemma 5.10

\underline{(1):} Since C is a (R, <)-choice-condition, we know that < is a wellfounded ordering on V_{∀} and R ⊆ V_{∃}×V_{∀}. Moreover, we have S_{e} ⊆ V_{∀}×V_{∃} and V_{∃}∩V_{∀} = ∅. Thus, if ⊲ is not wellfounded, then there is an infinitely descending sequence of the form y_{2i+2} S_{e} y_{2i+1} (R ∘ ≤) y_{2i} for all i ∈ IN. Since C is a (R, <)-choice-condition, we know that (R ∘ <) ⊆ R. Thus, we get y_{2i+2} S_{e} y_{2i+1} R y_{2i} for all i ∈ IN. This means that (S_{e}∘R)^{+} is not wellfounded, which contradicts the assumption that e is a strong existential (A, R)-valuation.

\underline{(2):} Let π ∈ (V_{∀}\dom(C)) → A. By noetherian induction on ⊲ and with the help of a choice function we can define some ϱ ∈ V_{free} → A in the following way: For x ∈ V_{∃}: ϱ(x) := e(x)(_{S_{e}⟨{x}⟩}|ϱ). For x ∈ V_{∀}\dom(C): ϱ(x) := π(x). For x ∈ dom(C): ϱ(x) := a, where a is an element of the universe of A such that, if possible, C(x) is not (_{V_{∀}}|ϱ, e, A)- valid. For this definition to be okay, we have to show, for each x ∈ V_{free}, that ϱ(x) is defined in terms of _{⊲⟨{x}⟩}|ϱ. In case of x ∈ V_{∃}, this is obvious because S_{e}⊆⊲. In case of x ∈ V_{∀}\dom(C), this is trivial. Thus, let x ∈ dom(C). Since C is a (R, <)-choice-condition, we have z^{∀} < x for all z^{∀} ∈ V_{∀}(C(x))\{x} and u^{∃} R x for all u^{∃} ∈ V_{∃}(C(x)). Thus, since R⊆⊲, by induction hypothesis, (_{V_{∀}}|ϱ, e, A)-validity of C(x) means validity of C(x) in A⊎ϱ. Moreover, since <⊆⊲, we know that ϱ(x) is defined in terms of _{V_{free}(C(x))\{x}}|ϱ ⊆ _{⊲⟨{x}⟩}|ϱ. Finally, we define ξ_{π} := _{dom(C)}|ϱ.

For showing that π⊎ξ_{π} is (e, A)-compatible with C, let y^{∀} ∈ dom(C) and suppose that C(y^{∀}) is (π⊎ξ_{π}, e, A)-valid, i.e. (_{V_{∀}}|ϱ, e, A)-valid. Thus, by definition of ϱ, we know that, for all η ∈ {y^{∀}} → A, C(y^{∀}) is (_{V_{∀}\{y^{∀}}}|ϱ⊎η, e, A)-valid, i.e. (π⊎_{V_{∀}\{y^{∀}}}|ξ_{π}⊎η, e, A)-valid. The rest is trivial.

\underline{(3a):} Let ξ be given as in (2). Define e′ via e′(x)(τ) := ξ_{π}(ς^{−1}(x)) (x ∈ ran(ς), τ ∈ ((V_{∀}\dom(C)) ∩ ⊲⟨{ς^{−1}(x)}⟩) → A, where π ∈ (V_{∀}\dom(C)) → A an arbitrary extension of τ) and e′(x)(τ) := e(x)(_{S_{e}⟨{x}⟩}|(π⊎ξ_{π})) (x ∈ V_{∃}\ran(ς), τ ∈ ((V_{∀}\dom(C)) ∩ ⊲⟨{x}⟩) → A, where π ∈ (V_{∀}\dom(C)) → A an arbitrary extension of τ). Note that this definition is okay because the choice of π does not matter: For the first π this is directly given by (2). For the second π we have: _{S_{e}⟨{x}⟩}|π ⊆ _{⊲⟨{x}⟩}|π ⊆ τ, and, for y ∈ dom(C) ∩ S_{e}⟨{x}⟩, by (2), ξ_{π}(y) is already determined by _{⊲⟨{y}⟩}|π ⊆ _{⊲⟨{x}⟩}|π ⊆ τ.

Then S_{e′} = _{V_{∀}\dom(C)}|id ∘ ( ⋃_{y∈ran(ς)} ⊲⟨{ς^{−1}(y)}⟩ × {y} ∪ ⋃_{x∈V_{∃}\ran(ς)} ⊲⟨{x}⟩ × {x} ).

Due to R′ = _{V_{∃}\ran(ς)}|id∘R ∪ ⋃_{y∈ran(ς)}{y} × ⟨{ς^{−1}(y)}⟩⊴ ∪ V_{∃}×dom(C), we get

S_{e′} ∘ R′ ⊆ _{V_{∀}\dom(C)}|id ∘

( ⋃_{y∈ran(ς)} ⊲⟨{ς^{−1}(y)}⟩ × ⟨{ς^{−1}(y)}⟩⊴ ∪ ⋃_{x∈V_{∃}\ran(ς)} (⊲⟨{x}⟩×{x}) ∘ R ∪ V^{∀}×dom(C))

⊆ _{V_{∀}\dom(C)}|id ∘ ( ⊲ ∪ V_{∀}×dom(C) ). Thus, (S_{e′}∘R′)^{+} is a wellfounded ordering because ⊲ is wellfounded by (1). This means that e′ is a strong existential (A, R′)-valuation. It now suffices to show that Gς is (τ, e′, A)-valid for all τ ∈ V_{∀} → A. Set π := _{V_{∀}\dom(C)}|τ. We get the following equalities for the below reasons:

eval(A ⊎ ϵ(e′)(τ) ⊎ τ)(Gς)  =
eval(A ⊎ ((_{V_{∃}}|id ⊎_{V_{∀}\dom(ς)}|id ⊎ ς) ∘ eval(A ⊎ ϵ(e′)(τ) ⊎ τ)))(G) =
eval(A ⊎ ϵ(e′)(τ) ⊎_{V_{∀}\dom(ς)}|τ ⊎ (ς∘(ϵ(e′)(τ))))(G)  =
eval(A ⊎ ϵ(e)(π ⊎ ξ_{π}) ⊎_{V_{∀}\dom(ς)}|τ ⊎_{dom(ς)}|ξ_{π})(G)  =
eval(A ⊎ ϵ(e)(π ⊎ ξ_{π}) ⊎ π ⊎ ξ_{π})(G)  =

TRUE

First: By the Substitution-Lemma. Second: By distributing ∘ over ∪. Third: Since, for x ∈ V_{∃}(G) we have x ∈ V_{∃}\ran(ς) and thus ϵ(e′)(τ)(x) = ϵ(e)(π ⊎ ξ_{π})(x). Moreover, since, for x ∈ dom(ς), ϵ(e′)(τ)(ς(x)) = ξ_{π}(ς^{−1}(ς(x))) = ξ_{π}(x), we get ς ∘ (ϵ(e′)(τ)) = dom(ς)|ξ_{π}. Fourth: By noting that dom(ς) = V_{∀}(G) ∩ dom(C). Fifth: Because π⊎ξ_{π} is (e, A)-compatible with C (by (2)) and G is C-strongly (e, A)-valid.

\underline{(3b):} When G is C-strongly R-valid in A, then there is some strong existential (R, A)- valuation e such that G is C-strongly (e, A)-valid. By (3a), Gς is ∅-strongly R′-valid in A. Since _{V_{∃}\ran(ς)}|R⊆R′′⊆R′, by Lemma 5.8, Gς is ∅-strongly _{V_{∃}\ran(ς)}|R-valid and ∅-strongly R′′-valid in A.

Q.e.d. (Lemma 5.10)

Proof of Lemma 5.12

(1), (2), (3), and (4) are trivial.

\underline{(5):} Let e′ be a strong existential (A, R′)-valuation and π be (e′, A)-compatible with C′ such that G_{1} is (π, e′, A)-valid. Let e be the strong existential (A, R)-valuation with ϵ(e) = ϵ(e′) given by Lemma 3.6(1) due to R⊆R′. Then π is (e, A)-compatible with C′, and G_{1} is (π, e, A)-valid. Moreover, due to C⊆C′, π is (e, A)-compatible with C. Thus, since G_{0} strongly (R, C)-reduces to G_{1}, also G_{0} is (π, e, A)-valid. This also means that G_{0} is (π, e′, A)-valid as was to be shown.

\underline{(6a):} Suppose that G_{0}σ is C′-strongly R′-valid in A. Then there is some strong existential (A, R′)-valuation e′ such that G_{0}σ is C′-strongly (e′, A)-valid. Then, by Lemma 3.6(2), there is some strong existential (A, R)-valuation e such that for all π ∈ V_{∀} → A: ϵ(e)(π) = σ∘eval(A ⊎ ϵ(e′)(π) ⊎ π). Moreover, for y ∈ V_{∀} we have: π(y) = eval(A ⊎ ϵ(e′)(π) ⊎ π)(y), i.e. ϵ(e)(π) ⊎ π = (σ ⊎_{V_{∀}}|id) ∘ eval(A ⊎ ϵ(e′)(π) ⊎ π). Thus, for any formula B, we have

eval(A ⊎ ϵ(e)(π) ⊎ π)(B)  =
eval(A ⊎ ((σ ⊎_{V_{∀}}|id) ∘ eval(A ⊎ ϵ(e′)(π) ⊎ π)))(B) =
eval(A ⊎ ϵ(e′)(π) ⊎ π)(Bσ),

the latter step being due to the Substitution-Lemma.

Thus, for any set of sequents G′ and any π ∈ V_{∀} → A:

(π, e, A)-validity of G′ is logically equivalent to (π, e′, A)-validity of G′σ. (:§_{1})

Especially, for any π ∈ V_{∀} → A:

π is (e, A)-compatible with C iff π is (e′, A)-compatible with C′. (:§_{2})

Thus, for any set of sequents G′:

G′ is C-strongly (e, A)-valid iff G′σ is C′-strongly (e′, A)-valid.

Especially, G_{0} is C-strongly (e, A)-valid. Thus, G_{0} is C-strongly R-valid in A.

\underline{(6b):} Let e′ be some strong existential (A, R′)-valuation, π be (e′, A)-compatible with C′, and suppose that G_{1}σ is (π, e′, A)-valid. Let e be the existential (A, R)-valuation given by Lemma 3.6(2). Then, by (§_{2}) in the proof of (6a), π is (e, A)-compatible with C, and, by (§_{1}) in the proof of (6a), G_{1} is (π, e, A)-valid. By assumption, G_{0} strongly (R, C)-reduces to G_{1}. Thus, G_{0} is (π, e, A)-valid, too. By (§_{1}) in the proof of (6a), this means that G_{0}σ is (π, e′, A)-valid as was to be shown.

Q.e.d. (Lemma 5.12)

Proof of Theor. 5.15 Since AX is ∅-strongly V_{∃}×V_{∀}-valid, t is closed, R ⊆ V_{∃}×V_{∀}, and ∅ ⊆ C, by Lemma 5.8, Goals({t}) is C-strongly R-valid. Since (Γ, t) ∈ F and (F, C, R, <) satisfies the invariant condition, {Γ } strongly (R, C)-reduces to Goals({t}). Then, by Lemma 5.12(1), Γ is C-strongly R-valid. Finally, by Lemma 5.10(3b), Γ ς is ∅-strongly R′-valid and ∅-strongly V_{∃}\ran(ς)|R-valid. Q.e.d. (Theor. 5.15)

Proof of Theor. 5.16

(∅, ∅, ∅, ∅) trivially satisfies the strong invariant condition. For the iteration steps, let (Γ′′, t′′) ∈ F′. Assuming the strong invariant condition for (F, C, R, <), we have to show that C′ is a (R′, <′)-choice-condition and that {Γ′′} strongly (R′, C′)-reduces to Goals({t′′}).

\underline{Hypothesizing:} Due to the assumed R∘< ⊆ R and the required R′′∘< ⊆ R′ = R∪R′′, we have R′ ∘ < = (R∪R′′) ∘ < ⊆ R∪R′′ = R′. Thus, C is a (R′, <)-choice-condition. Moreover, due to C′ = C and <′ = <, (C′, R′, <′) is an extension of (C, R, <). In case of (Γ′′, t′′) ∈ F, {Γ′′} (R, C)-reduces to Goals({t′′}) by assumption, and then, due to Lemma 5.12(5), {Γ′′} strongly (R′, C′)-reduces to Goals({t′′}). Otherwise we have (Γ′′, t′′) = (Γ, t). Then {Γ′′} = {Γ } = Goals({t}) = Goals({t′′}). Thus, by Lemma 5.12(2), {Γ′′} strongly (R′, C′)-reduces to Goals({t′′}).

\underline{Expansion:} In case of (Γ′′, t′′) ∈ F, \{Γ′′\} (R, C)-reduces to Goals(\{t′′\}) by assumption, and then, due to (C′, R′, <′) being an extension of (C, R, <) and Lemma 5.12(5), {Γ′′} strongly (R′, C′)-reduces to Goals({t′′}). Otherwise we have (Γ′′, t′′) = (Γ, t′). Since Goals({t})\{Δ} ⊆ Goals({t′}), by Lemma 5.12(2), Goals({t})\{Δ} strongly (R′, C′)- reduces to Goals({t′}). Thus, since by assumption {Δ} strongly (R′, C′)-reduces to a subset of Goals({t′}), by Lemma 5.12(4) Goals({t}) strongly (R′, C′)-reduces to Goals({t′}). Moreover, due to (Γ, t) ∈ F, by assumption {Γ } strongly (R, C)-reduces to Goals({t}). Thus, by Lemma 5.12(5), {Γ } strongly (R′, C′)-reduces to Goals({t}). Thus, since Goals({t}) strongly (R′, C′)-reduces to Goals({t′}), by Lemma 5.12(3), {Γ } strongly (R′, C′)-reduces to Goals({t′}), i.e. {Γ′′} strongly (R′, C′)-reduces to Goals({t′′}).

\underline{Instantiation:} By Lemma 5.5, C′ is a (R′, <′)-choice-condition. There is some (Γ, t) ∈ F such that (Γ, t)σ = (Γ′′, t′′). By assumption, {Γ } strongly (R, C)-reduces to Goals({t}). By Lemma 5.12(6b), {Γ σ} strongly (R′, C′)-reduces to Goals({t})σ, i.e. {Γ′′} strongly (R′, C′)-reduces to Goals({t′′}).

Q.e.d. (Theor. 5.16)

Proof of Theor. 5.17

Let A be an arbitrary Σ-structure (Σ-algebra). We only prove the first example of each kind of rule to be a sub-rule of the Expansion rule and leave the rest as an exercise.

\underline{α-rule:} We have to show that \{Γ (A∨B) Π\} strongly (R, C)-reduces to \{A B Γ Π\} in A. This is trivial, however, because (π, e, A)-validity of the two sets is logically equivalent for each strong existential (A, R)-valuation e and π ∈ V_{∀} → A.

\underline{β-rule:} We have to show that \{Γ (A∧B) Π\} strongly (R, C)-reduces to \{A Γ Π, B Γ Π\} in A. This is trivial, however, because (π, e, A)-validity of the two sets is logically equivalent for each strong existential (A, R)-valuation e and π ∈ V_{∀} → A.

\underline{γ-rule:} We have to show that \{Γ ∃x:A Π\} strongly (R, C)-reduces to \{A\{x↦x^{∃}\} Γ ∃x:A Π\} in A. This is the case, however, because (π, e, A)-validity of the two sets is logically equivalent for each strong existential (A, R)-valuation e and π ∈ V_{∀} → A. The direction from left to right is given because the former sequent is a sub-sequent of the latter. The other direction, which is the only one we actually have to show here, is also clear because (π, e, A)- validity of A{x↦x^{∃}} implies (π, e, A)-validity of ∃x: A. Although this is clear, we should be a little more explicit here because the standard semantic definition of ∃ (cf. e.g. Wirth (1997), p. 188) does not use free existential variables and is somewhat more complicated than it could be in terms of free existential variables. Moreover, in the note above the theorem we remarked that the restriction on x^{∃} not occurring in the former sequent is not really necessary. Thus, in order to be more explicit here, assume that the latter sequent is (π, e, A)-valid for some strong existential (A, R)-valuation e and some π that is (e, A)-compatible with C. We have to show that the former sequent is (π, e, A)-valid. If this is not the case, A{x↦x^{∃}} must be (π, e, A)-valid. Let y^{∀} ∈ V_{∀}\V_{∀}(A). Then, since A{x↦y^{∀}}{y^{∀}↦x^{∃}} is equal to A{x↦x^{∃}}, we know that A{x↦y^{∀}}{y^{∀}↦x^{∃}} is valid in A ⊎ ϵ(e)(π) ⊎ π. Then, by the Substitution-Lemma, A{x↦y^{∀}} is valid in A ⊎ ϵ(e)(π) ⊎ π′ for π′ ∈ V_{∀} → A given by _{V_{∀}\{y^{∀}}}|π′ := _{V_{∀}\{y^{∀}}}|π and π′(y^{∀}) := ϵ(e)(π)(x^{∃}). By the standard semantic definition of ∃ and since quantification on x cannot occur in A (as ∃x: A is a formula in our restricted sense, cf. Section 1.4), this means that ∃x:(A{x↦y^{∀}}{y^{∀}↦x}) is valid in A ⊎ ϵ(e)(π) ⊎ π. Since y^{∀} does not occur in A, this formula is equal to ∃x:A, which means that the former sequent is (π, e, A)-valid as was to be shown.

\underline{δ-rule:} Firstly, we have to show that C′ is a (R′, <′)-choice-condition. Since x^{∀} ∉ V_{∀}(A) ∪ dom(<) and < is a wellfounded ordering, <′ := < ∪ ≤⟨V_{∀}(A)⟩ × {x^{∀}} is a wellfounded ordering with x^{∀} ∉ dom(<′), too. Therefore, R′′ ∘ <′ = ∅, and then R′ ∘ <′ = (R ∪ R′′) ∘ <′ = R ∘ <′ = R ∘ (< ∪ <′′) = (R ∘ <) ∪ (R ∘ <′′) ⊆ R ∪ R′′ = R′; where the inclusion is due to the following: first, we have R ∘ < ⊆ R because C is a (R, <)-choice-condition; second, in case of z_{0} R z_{1} <′′ z_{2} we have z_{2} = x^{∀} and there is some z′ ∈ V_{∀}(A) with z_{1} ≤ z′; then, again by R ∘ < ⊆ R, we get z_{0} R z′, i.e. z_{0} R′′ x^{∀} = z_{2}. Since < ⊆ <′, R ⊆ R′, C′ = C ∪ {(x^{∀}, A{x↦x^{∀}})}, V_{∀}(C′(x^{∀}))\{x^{∀}} = V_{∀}(A{x↦x^{∀}})\{x^{∀}} = V_{∀}(A)\{x^{∀}} = V_{∀}(A) ⊆ <′⟨{x^{∀}}⟩, and V_{∃}(C′(x^{∀})) = V_{∃}(A{x↦x^{∀}}) = V_{∃}(A) ⊆ R′⟨{x^{∀}}⟩, the remaining requirements for C′ to be a (R′, <′)-choice-condition are easily checked.

Secondly, we have to show that {Γ ∀x:A Π} strongly (R′, C′)-reduces to {A{x↦x^{∀}} Γ Π} in A. Assume that the latter sequent is (π, e, A)-valid for some strong existential R′-valuation e and some π that is (e, A)-compatible with C′. We have to show that the former sequent is (π, e, A)-valid. If some formula in Γ Π is (π, e, A)-valid, then the former sequent is (π, e, A)-valid, too. Otherwise, this means that A{x↦x^{∀}} is (π, e, A)-valid. Since π is (e, A)-compatible with C′, A{x↦x^{∀}} is (π′, e, A)-valid for all π′ ∈ V_{∀} → A with V_{∀}\{x^{∀}}|π′ = _{V_{∀}\{x^{∀}}}|π. Since V_{∃}(A{x↦x^{∀}}) × {x^{∀}} = V_{∃}(A) × {x^{∀}} ⊆ R′, we know that A{x↦x^{∀}} is even valid in A ⊎ ϵ(e)(π) ⊎ π′ for all π′ ∈ V_{∀} → A with _{V_{∀}\{x^{∀}}}|π′ = _{V_{∀}\{x^{∀}}}|π. By the standard semantic definition of ∀ (cf. e.g. Wirth (1997), p. 188) and since quantification on x cannot occur in A (as ∀x:A is a formula in our restricted sense, cf. Section 1.4), this means that ∀x:(A{x↦x^{∀}}{x^{∀}↦x}) is valid in A ⊎ ϵ(e)(π) ⊎ π. Since x^{∀} does not occur in A, this formula is equal to ∀x:A, which means that the former sequent is (π, e, A)-valid as was to be shown.

Q.e.d. (Theor. 5.17)

References and Notes

Matthias Baaz, Christian G. Fermüller (1995). Non-elementary Speedups between Different Versions of Tableaux. 4^{th}TABLEAUX 1995, LNAI 918, pp. 217-230, Springer.

Peter Baumgartner, Ulrich Furbach, Frieder Stolzenburg (1997). Computing Answers with Model Elimination. Artificial Intelligence 90, pp. 135-176.

Bernhard Beckert, Reiner Hähnle, Peter H. Schmitt (1993). The Even More Liberalized δ-Rule in Free Variable Semantic Tableaux. Kurt Gödel Colloquium, LNCS 713, pp. 108-119, Springer.

Wolfgang Bibel (1987). Automated Theorem Proving. 2^{nd} rev. ed., Vieweg, Braunschweig.

Wolfgang Bibel, Peter H. Schmitt (eds.) (1998). Automated Deduction — A Basis for Applications. Kluwer Acad. Publ..

N. Bourbaki (1954). Livre I — Théorie des Ensembles. Hermann, Paris.

Hans-Jürgen Bürckert, Bernhard Hollunder, Armin Laux (1993). On Skolemization in Constrained Logics. DFKI Research Report RR–93–06, Saarbrücken. Also in: Annals of Mathematics and Artificial Intelligence 18, pp. 95-131, Balzer Sci. Publ., 1996.

Henk Doornbos, Roland Backhouse, Jaap van der Woude (1997). A Calculational Approach to Mathematical Induction. Theoretical Computer Sci. 179, pp. 103-135, Elsevier.

Melvin Fitting (1996). First-Order Logic and Automated Theorem Proving. 2^{nd} extd. ed., Springer.

Gerhard Gentzen (1935). Untersuchungen über das logische Schließen. Mathematische Zeitschrift 39, pp. 176-210, 405-431.

Reiner Hähnle, Peter H. Schmitt (1994). The Liberalized δ-Rule in Free Variable Semantic Tableaux. J. Automated Reasoning 13, pp. 211-221, Kluwer Acad. Publ..

S. Kanger (1963). A Simplified Proof Method for Elementary Logic. In: Siekmann & Wrightson (1983), Vol. 1, pp. 364-371.

Donald E. Knuth (1997). The Art of Computer Programming. Vol. 1, 3^{rd} edition, Addison-Wesley.

Michaël Kohlhase (1995). Higher-Order Tableaux. 4^{th}TABLEAUX 1995, LNAI 918, pp. 294-309, Springer. Revised version is: Kohlhase (1998).

Michaël Kohlhase (1998). Higher-Order Automated Theorem Proving. In: Bibel & Schmitt (1998), Vol. 1, pp. 431-462.

Dale Miller (1992). Unification under a Mixed Prefix. J. Symbolic Computation 14, pp. 321-358, Academic Press.

Andreas Nonnengart (1996). Strong Skolemization. MPI–I–96–2–010, Max-Planck-Institut für Informatik, Saarbrücken.

Michael S. Paterson, Mark N. Wegman (1978). Linear Unification. J. Computer and System Sci. 16, pp. 158-167, Academic Press.

Dag Prawitz (1960). An Improved Proof Procedure. In: Siekmann & Wrightson (1983), Vol. 1, pp. 159-199.

Jörg Siekmann, G. Wrightson (eds.) (1983). Automation of Reasoning. Springer.

Raymond M. Smullyan (1968). First-Order Logic. Springer.

Claus-Peter Wirth (1997). Positive/Negative-Conditional Equations: A Constructor-Based Framework for Specification and Inductive Theorem Proving. Dissertation (Ph.D. thesis), Verlag Dr. Kovač, Hamburg.

Claus-Peter Wirth (1998). Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized δ-Rule but Without Skolemization. In: Gernot Salzer, Ricardo Caferra (eds.). Proc. 2^{nd} Int. Workshop on First-Order Theorem Proving (FTP), pp. 244-255, Vienna.

Claus-Peter Wirth (1999). Full First-Order Free Variable Sequents and Tableaux in Implicit Induction. 8^{th}TABLEAUX 1999, LNAI 1617, pp. 293-307, Springer.

Claus-Peter Wirth, Klaus Becker (1995). Abstract Notions and Inference Systems for Proofs by Mathematical Induction. 4^{th}CTRS 1994, LNCS 968, pp. 353-373, Springer.

Claus-Peter Wirth, Bernhard Gramlich (1994). On Notions of Inductive Validity for First-Order Equational Clauses. 12^{th}CADE 1994, LNAI 814, pp. 162-176, Springer.

1For Skolemization in constrained logics cf. Bürckert & al. (1993), where, however, only the existence of solutions of constraints and not the form of the solutions itself is preserved.

2While this paradigm of inductive theorem proving was already used by the Greeks, Pierre de Fermat (1601-1665) rediscovered it under the name “descente infinie”, and in our time it is sometimes called “implicit induction”, cf. Wirth & Becker (1995), Wirth (1997).

3The notation ⟨A⟩R is in the tradition of Bourbaki (1954), Chapitre II, § 3, Définition 3, where R⟨A⟩ is written in order to clearly distinguish relation application ⟨A⟩R from function application R(A). In Wirth (1997) we still used to write R[A] instead of ⟨A⟩R. In this paper, however, this notation would lead to confusion with our use of optional brackets.

4We do not need the more complicated definitions of a sequent as a pair of lists of formulas or as a T/F-tagged list of formulas because we do not consider calculi where the separation of a sequent into antecedent and succedent is important, like LJ in Gentzen (1935) or the “symmetric Gentzen systems” in Smullyan (1968).

5Note that R^{−1} is an inverse (in the sense that R∘R^{−1} =_{dom(R)}|id and R^{−1}∘R = ran(R)|id holds) iff R is an injective function.

6For the notion of a tree cf. Knuth (1997). As a special feature we would like an explicit representation of leaves, such that, when we add the elements of a set G as children to a leaf node l, this l is not a leaf anymore, even if G is empty.

7Note that this restriction on x^{∃} is not required for soundness (cf. Theor. 4.11) but for efficiency only.

8Note that this restriction on x^{∃} is not required for soundness (cf. Theor. 5.17) but for efficiency only.

9Actually, when E_{σ} is efficiently added to the graph representing R and U_{σ} in order to represent R′ := E_{σ} ∘ R ∘ (U_{σ}∘R)^{∗}, an element (u^{∃}, x^{∃}) ∈ E_{σ} is simply implemented by drawing a new edge from the (possibly new) node for u^{∃} to the old node for x^{∃}. (u^{∃} gets a new node iff (u^{∃}, u^{∃}) ∉ E_{σ}.) Although this graph is not really bipartite in V_{∃}- and V_{∀}-nodes, when checking for acyclicity of U_{σ′}∘R′, when finding a new V_{∃}-node to be already on the active path, we can detect a cycle of V_{∃}-nodes simply by asking whether we are coming from a V_{∃}-node, in which case we skip the new V_{∃}-node and do not signal a cycle of U_{σ′}∘R′.

10We have very recently presented these calculi at the 2^{nd} Int. Workshop on First-Order Theorem Proving (FTP) in Nov. 1998 in Vienna (cf. Wirth (1998)), where nobody in the audience was able to point out other work in this direction.

Acknowledgements: I would like to thank Ulrich Furbach and his whole group for all they taught me on tableau calculi. Furthermore, I would like to thank Michaël Kohlhase for his encouragement to drop Skolemization and Peter Padawitz for the possibility to finish this work. Finally, I am indebted to an anonymous referee for his careful reading of a short version of this paper and his most useful remarks.