Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized δ-Rule but Without Skolemization, and now including Lemma Application

Claus-Peter Wirth

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

Research Report LS5.cs.uni-dortmund.de/˜ wirth/p/gr698/new/all.ps.gz February 8, 2000 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. Lemma application is now included into all calculi.

Contents

1 Introduction 1 1.1 Sequent and Tableau Calculi . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 Some Inference Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.3 Without Skolemization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.4 Preservation of Solutions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.5 Variables, Formulas, Sequents, and Substitutions . . . . . . . . . . . . . . . . 7 1.6 The Liberalized δ-rule . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

2 Basics 10

3 Variable-Conditions 11

4 The Weak Version 14 4.1 Validity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 4.2 Reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 4.3 Abstract Sequent and Tableau Calculus . . . . . . . . . . . . . . . . . . . . . 16 4.4 Concrete Sequent and Tableau Calculus . . . . . . . . . . . . . . . . . . . . . 19

5 The Strong Version 22 5.1 Why is it so difficult? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 5.2 Choice-Conditions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 5.3 Strong Validity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 5.4 Strong Reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 5.5 Abstract Sequent and Tableau Calculus . . . . . . . . . . . . . . . . . . . . . 27 5.6 Concrete Sequent and Tableau Calculus . . . . . . . . . . . . . . . . . . . . . 29

6 Conclusion and Outlook 33

The Proofs 34

References and Notes 51

1 Introduction

When first-order validity is introduced to students it comes with some complete calculus. If this calculus happens to be an analytic calculus augmented with a Cut rule like a sequent or tableau calculus, the students can compare the formal proofs with the informal ones they are hopefully acquainted with. To our opinion, these calculi can mirror the human proof search process better than others. While knowing a complete calculus does not mean to know much about first-order theorem proving, the interrelation of a human-oriented calculus and the informal proof search of the students will turn out to be fruitful for their later mathematical work. It is a pity that—while nearly all proofs of a working mathematician include induction—nothing comparable for inductive first-order validity is offered to the students. Some may argue that this is generally impossible because not even the first-order theory of the Peano algebra of natural numbers is recursively enumerable, cf. e.g. Enderton (1973). Nevertheless, there really is some general way in that many working mathematicians search for an informal proof, may it be inductive or not. The inductive version of this proof search method goes back to the ancient Greeks and was rediscovered under the name “descente infinie” by Pierre de Fermat (1601-1665). If you want to prove a conjecture, this method requires that you show, for each assumed counterexample of the conjecture, the existence of another counterexample of the conjecture that is strictly smaller in some wellfounded ordering. The working mathematician applies it in the following fashion.

He (who may be female!) starts with the conjecture and simplifies it in case analyses which can be described as steps in a sequent or tableau calculus with Cut. When he realizes that the goals become similar to a different instance of the conjecture, he applies the conjecture just like a lemma, but keeps in mind that he actually has applied some induction hypothesis. Finally, he searches for some wellfounded ordering in which all the instances of the conjecture that he has applied as induction hypotheses are smaller than the original conjecture itself.

In this paper we show how deductive first-order theorem proving should look like from the point of view of induction in the style of “descente infinie”. While many possible choices in the design of calculi for deductive theorem proving do not really matter because the alternatives are dual to each other, they do make an important difference when one wants to integrate inductive theorem proving.

Nevertheless, even the researcher who is not interested in induction can learn something on answer computation, on lemma application, and on the details of the difference between the δ-rule and the liberalized δ-rule (δ^{+}) that become obvious when the preservation of solutions (closing substitutions) is considered besides soundness.

The paper organizes as follows: After explaining the technical terms of the title in the rest of 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. Please do try not to read the notes on a first reading!

1.1 Sequent and Tableau Calculi

We assume familiarity with first-order analytic theorem proving. We recommend Gentzen (1935) and Fitting (1996) as excellent introductions to this subject.

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

α-rules describe the simple and

β-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.

Other rules may be added for an appropriate treatment of often used reasoning like equality reasoning etc..

1.2 Some Inference Rules

Although the following inference rules cannot be completely understood on a first reading, they may clear away some fog. They are presented in the sequent calculus style. Moreover, note that in old times when trees grew upwards, Gerhard Gentzen would have written the inference rules such that passing the line meant implication. We have inverted the rules. Thus, in our case, passing the line means reduction.

Let A and B be formulas, Γ, Π, and Λ be sequents, x ∈ V_{bound} a bound variable, and (F, C, R, L) the current proof forest containing all free variables already used, esp. those from A and Γ Π:

α-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: Let x^{∃} ∈ V_{∃} \ V(F, C, R, L) be a new^{1} free existential variable:

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

δ-rules: Let x^{∀,w} ∈ V_{∀,w}\V(F, C, R, L) be a new (i.e. at least^{2} not from V(A, Γ Π)∪dom(R)) weak free universal variable:

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

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

Liberalized δ-rules: Let x^{∀,s} ∈ V_{∀,s} \ V(F, C, R, L) be a new (i.e. at least^{3} not from V(A) ∪ dom(C∪R)) strong free universal variable:

\frac{Γ ∀x: A Π}{A\{x↦x^{∀,s}\} Γ Π}  \begin{matrix}\{(x^{∀,s}, A\{x↦x^{∀,s}\})\} \\ V_{free}(A) × \{x^{∀,s}\} \end{matrix}

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

Rewrite-Rules: Let s and t be terms (of the same sort). Let B be one of the formulas (s≠t) or (t≠s). Let A[t] denote the formula A[s] with some occurrences of s replaced with t:

\frac{Γ A[s] Π B Λ}{A[t] Γ Π B Λ}  \frac{Γ B Π A[s] Λ}{A[t] Γ B Π Λ}

1.3 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^{4} 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 for T (e⃗, u⃗),

∀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. While this paradigm of inductive theorem proving was already used by the ancient 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). The reason why this quantification structure does not go together with descente infinie is that the induction hypothesis applications may destroy the counterexample:

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 for different branches. 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, the induction hypothesis application of descente infinie works well:

When, for some (fixed) e⃗_{0}, we have some counterexample u⃗ for T (e⃗_{0}, u⃗) (i.e. T (e⃗_{0}, 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⃗_{0} 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⃗_{0}.

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.4 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 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 (cf. Hilbert & Bernays (1968/70), Vol. II), 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.

Suppose that our original input theorem T (e⃗, u⃗) (cf. the discussion in Section 1.3) has been reduced to R(e⃗, u⃗) representing the state of the proof attempt. With “preservation of solutions” we mean that, for any solution e⃗_{0},

R(e⃗_{0}, u⃗) implies T (e⃗_{0}, u⃗) for each u⃗. ($)

This is again closely related to inductive theorem proving:

Suppose that we have found some solution e⃗_{0} such that for each counterexample u⃗ of R(e⃗_{0}, u⃗) there is a counterexample u′ for the original theorem (i.e. T (e⃗_{0}, u′) is invalid) and that this u′ is strictly smaller than u⃗ in some wellfounded ordering.

In this case we have proved T (e⃗_{0}, u⃗) (and thus T (e⃗, u⃗)) only if

each counterexample u⃗ for T (e⃗_{0}, u⃗) is also a counterexample for R(e⃗_{0}, u⃗).

The latter is the contrapositive of ($) and therefore logically equivalent to it.

1.5 Variables, Formulas, Sequents, and Substitutions

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

\begin{aligned}dom(R) & := & \{ a | ∃b: (a, b) ∈ R \} & ; \\ ran(R) & := & \{ b | ∃a: (a, b) ∈ R \} & ; \\ _{A}|R & := & \{ (a, b) ∈ R | a ∈ A \} & ; \\ R|_{B} & := & \{ (a, b) ∈ R | b ∈ B \} & ; \\ ⟨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.^{6} 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 A again, unless A has the form ¬¬B.

In the tradition of Gentzen (1935) we assume the following four sets of symbols to be disjoint:

V_{∃}  free existential variables,

i.e. the free variables of Fitting (1996)

V_{∀}  free universal variables,

i.e. nullary parameters, our substitute for Skolem functions

V_{bound} bound variables,

i.e. variables for quantified use only

Σ  constants,

i.e. the function (and predicate) symbols from the signature

We split the free universal variables into weak free universal variables that behave as in the weak version of Wirth (1998a) and are introduced by the non-liberalized δ-rules; and strong free universal variables that behave as in the strong version and are introduced by the liberalized δ-rules:

V_{∀} = V_{∀,w} ⊎ V_{∀,s}.

We define the free variables by

V_{free} := V_{∃} ⊎ V_{∀}.

For k being any of these kinds of variables and for a term, formula, sequent Γ etc., ‘V_{k}(Γ)’ denotes the set of variables from V_{k} occurring in Γ. Moreover, we assume each V_{k} to be infinite (for each sort) and that any formula contains only finitely many variables.

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. Moreover, we require that variables from V_{bound} do not occur unbound in any formula.

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 σ.

1.6 The Liberalized δ-rule

Definition 1.1 (Variable-Condition) A variable-condition is a subset of V_{free} × V_{free}.

Roughly speaking, for a variable-condition R, (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 the free universal variable 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.2 ∃x: ∀y: (x = y)

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

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

δ-step:

(x^{∃} = y^{∀}), ∃x: ∀y: (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.3 ∃x: ( P(x) ∨ ∀y: ¬P(y) ) can be proved the following way:

γ-step:

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

α-step:

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

Liberalized δ-step:

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

Instantiation step:

P(y^{∀,s}), ¬P(y^{∀,s}), ∃x: ( P(x) ∨ ∀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^{∀,s} do not depend on each other and there is no reason to insist on x^{∃} being older than y^{∀,s}. 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^{∀,s} 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.3 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.4 and Kohlhase (1998) w.r.t. our Ex. 5.21. The difficulty lies with instantiation steps that relate previously unrelated variables:

Example 1.4

∃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^{∀,s}), ¬Q(v^{∀,s}, u^{∃}), ∃x: ∀y: Q(x, y), ∃u: ∀v: ¬Q(v, u) (∗)

with variable-condition

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

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

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

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

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

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^{∀,s}(u^{∃}) in

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

we get

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

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

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

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

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

\begin{matrix}u^{∃} & \overline{_{_{R} >}} & v^{∀,s} \\ y^{∀,s} & ∧_{σ^{−1}} & < _{R} & x^{∃} & ^{∨^{σ^{−1}}} \end{matrix}

must not exist. Although this seems to be fairly difficult, the formal treatment—once discovered—is quite simple.

2 Basics

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^{7} 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. Functions are nothing but (right-) unique relations and the meaning of ‘f∘g’ does not depend on f and g being only relations or even functions. Thus, ‘(f∘g)(x)’ means ‘g(f(x))’.

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 non-empty 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). 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, valuation π ∈ V_{free} → A, and term or formula B:

eval(A⊎π)(Bσ) = eval( A ⊎ ( σ ⊎ _{V_{free}\dom(σ)}|id ) ∘ eval(A⊎π) )( B ). Note that we assume the operator ‘∘’ to have higher priority than the operators ‘∪’ and ‘⊎’. 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 Variable-Conditions

In this section we formally describe two possible choices for the formal treatment of variable-conditions. The weak version works well only 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_{σ} := { (z^{∃}, x^{∃}) | z^{∃} ∈ V_{∃}(σ(x^{∃})) ∧ x^{∃} ∈ dom(σ) }

and the universal relation to be

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

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 (R ∪ U_{σ} ∪ E_{σ})^{+} 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 Rsubstitution is quite straightforward. The definition of a strong existential R-substitution requires an additional transitive closure because the strong version then admits a smaller R. To see this, take from Ex. 1.4 the variable-condition R of (#) and the σ of ($). As explained there, σ must not be a strong existential R-substitution due to the cycle

\begin{matrix}u^{∃} & \overline{_{_{R} >}} & v^{∀,s} \\ y^{∀,s} & ∧_{U_{σ}} & < _{R} & x^{∃} & ^{∨^{U_{σ}}} \end{matrix}

which just contradicts the irreflexivity of (R ∪ U_{σ} ∪ E_{σ})^{4}. Note that in practice w.l.o.g. R, U_{σ}, and E_{σ} can always be chosen to be finite, so that irreflexivity of (R ∪ U_{σ} ∪ E_{σ})^{+} is then equivalent to (R ∪ U_{σ} ∪ E_{σ})^{+} 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 R and U_{σ} again.

Definition 3.3 ([Strong] σ-Update)

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

The σ-update of R is R ∪ E_{σ}∘R.

The strong σ-update of R is R ∪ E_{σ} ∪ U_{σ}.

Example 3.4

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

σ′ := {x^{∃}↦v^{∀,s}}

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

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

and

E_{σ′} = ∅.

Thus, the strong σ′-update of R is then given by the following graph whose transitive closure is irreflexive and thus a wellfounded ordering.

\begin{matrix}u^{∃} & \overline{_{_{R} >}} & v^{∀,s} \\ y^{∀,s} & < _{R} & x^{∃} & ^{∨^{U_{σ′}}} \end{matrix}

Note that the variable-conditions of the strong version are very close to an implementation. For efficiency reasons we should never compute transitive closures but simply keep adding new edges to a graph. The relevant wellfoundedness checks can then be performed as cyclicity checks, which have a time complexity that is linear in the number of edges.

For simplicity of implementation we even have made re-use of free existential variables and name switches like {x^{∃}↦u^{∃}, u^{∃}↦x^{∃}} impossible because all these substitutions lead to a cycle in the existential relation and thus are no strong existential R-substitutions. Reuse of free existential variables and name switches are not appropriate in practice because then we need a time reference in addition to the variable name to retrieve its solutions or values.^{8} 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: V_{∃} → ((V_{∀} ⇝ A) ⇝ A), at most one semantic relation exists, namely

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

Definition 3.5 (Semantic Relation (S_{e})) Let e: X → ((Y ⇝ A) ⇝ A). The semantic relation of e is S_{e} := { (y, x) | y ∈ dom(⋃(dom(e(x)))) ∧ x ∈ X }. e is semantic if e(x): (S_{e}⟨{x}⟩ → A) → A for all x ∈ X.

Definition 3.6 ([Strong] Existential (A, R)-Valuation)

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

e is an existential (A, R)-valuation if e is semantic and S_{e} ∘ R is irreflexive.

e is a strong existential (A, R)-valuation if e is semantic and (R ∪ S_{e})^{+} is a wellfounded ordering.

Finally, for applying [strong] existential (A, R)-valuations in a uniform manner:

Definition 3.7 (ϵ) We define the function

ϵ: (X → ((Y ⇝ A) ⇝ A)) ⇝ ((Y → A) → (X → A))

by ( e ∈ X → ((Y ⇝ A) ⇝ A) being semantic, π ∈ Y → A, x ∈ X )

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

Lemma 3.8 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 S_{e} = S_{e′} and ϵ(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 S_{e} = S_{e′} ∘ (_{V_{∃}\dom(σ)}|id ∪ E_{σ}) ∪ U_{σ}

and for all π ∈ V_{∀} → A:

ϵ(e)(π) = (_{V_{∃}\dom(σ)}|id ∪ σ) ∘ eval(A ⊎ ϵ(e′)(π) ⊎ π).

4 The Weak Version

In this section we treat all free universal variables as if they were weak, i.e. from V_{∀,w}. This gives the readers a chance to understand the basic concepts without the added difficulty of the strong free universal variables that are necessary for the liberalized versions of the δrule and for “answer computation”. Since the strong free universal variables are not treated properly in this section, we assume that they do not occur in any proof tree.

4.1 Validity

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.

Example 4.2 (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^{∀}) for π ∈ V_{∀} → A, 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}.

4.2 Reduction

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.3 (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.4 (Reduction)

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

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′:

(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.

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.

4.3 Abstract Sequent and Tableau Calculus

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.5 (Proof Forest) A (deductive) proof forest in a sequent (or else: tableau) calculus is a quadruple (F, ∅, R, L) where the second component is empty, R is a variable-condition, L ⊆ IN_{+}×IN_{+}, and F is a partial function from IN_{+} into the set of pairs (Γ, t), where Γ is a sequent and t is a tree^{9} whose nodes are labeled with sequents (or else: formulas).

Note that the tree t is intended to represent a proof attempt for Γ. Furthermore, L records the lemma applications in the sense that j L i means that Γ_{j} has been applied as lemma in the proof tree t_{i} of Γ_{i} for (Γ_{i}, t_{i}) := F (i) and (Γ_{j}, t_{j}) := F (j).

The nodes of a tree 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.6 (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. (By Lemma 4.4(5a), this means that AX is R-valid for any variable-condi-tion R. For the missing reference to a Σ-structure, cf. the last sentence in Def. 4.1.) Typically, AX contains all sequents of the forms Γ A Π \overline{A} Λ and Γ (t=t) Π for sequents Γ, Π, Λ, formulas A, and terms t. 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 two trees (i, (Γ, t)), (i′, (Γ′, t′)) ∈ F we can apply Γ′ as a lemma in the tree t of Γ and record this lemma application by inserting (i′, i) into L. Provided that the lemma application relation L is acyclic and all trees (i′′, (Γ′′, t′′)) with i′′L^{∗}i are closed, this proves that Γ is R-valid. For deductive theorem proving the availability of lemma application is not really necessary. For inductive theorem proving (descente infinie), however, lemma and induction hypothesis application of this form becomes necessary.

The following invariant condition captures the soundness of our proof trees. Roughly speaking (when no lemma has been applied), the validity of the goals of a tree is to imply the validity of the sequent of this tree; short: “The leaves imply the root.”

Definition 4.7 (Soundness Invariant Condition) The soundness invariant condition on (F, ∅, R, L) is that, for all (i, (Γ, t)) ∈ F,

{Γ } R-reduces to Goals({ t′ | (i′, (Γ′, t′)) ∈ F ∧ i′L^{∗}i }).

Note that { t′ | (i′, (Γ′, t′)) ∈ F ∧ i′L^{∗}i } contains exactly the tree t as long as no lemmas have been applied in t.

Theorem 4.8 (Successful Proof) Let the proof forest (F, ∅, R, L) satisfy the above soundness invariant condition. Let (i, (Γ, t)) ∈ F. If all trees in { t′ | (i′, (Γ′, t′)) ∈ F ∧ i′L^{∗}i } are closed, then Γ is R-valid.

In the following definition, abstract proof steps of the following three different kinds are considered: A Hypothesizing step starts a new proof tree for a new conjecture; an Expansion step expands a proof tree; and an Instantiation step globally instantiates some free existential variables in the whole proof forest.

Definition 4.9 (Abstract Sequent (or else: Tableau) Calculus)

We start with the empty proof forest (F, ∅, R, L) := (∅, ∅, ∅, ∅) and then iterate only the following kinds of modifications of (F, ∅, R, L) (resulting in (F′, ∅, R′, L′)):

Hypothesizing: Let R′ be a variable-condition with R⊆R′. Set L′ := L.

Let i ∈ IN_{+} \ dom(F). 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 ∪ {(i, (Γ, t))}.

Expansion: Let (i, (Γ, t)) ∈ F. Let R′ be a variable-condition with R⊆R′. Let N ⊆ dom(F) such that L^{∗} ∩ ({i}×N) = ∅. 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 ∪ dom(⟨N⟩F) (or else: { ΛΔ | Λ ∈ G } ∪ dom(⟨N⟩F)), then we may set L′ := L ∪ N×{i} and F′ := (F \{(i, (Γ, t))}) ∪ {(i, (Γ, 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 L′ := L and F′ := { (i, (Γ σ, tσ)) | (i, (Γ, t)) ∈ F }.

While Hypothesizing and Instantiation steps are self-explanatory, Expansion steps are parameterized by a sequent Δ, a set N ⊆ dom(F), and a set of sequents G such that {Δ} R′-reduces to G ∪ dom(⟨N⟩F). While dom(⟨N⟩F) contains some sequents from other proof trees which are applied as lemmas, the sequents in G become the new child nodes of the former leaf node labeled with Δ.

For tableau calculi, however, this set G 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.

Theorem 4.10 (Soundness) The above soundness invariant condition is always satisfied for the sequent (or else: tableau) calculus of Def. 4.9.

While the soundness invariant condition of Def. 4.7 (“the leaves imply the root”) is an essential one, the converse, namely “the root implies the leaves”, which we call safeness, is useful in practice for failure detection.

Suppose we have disproved (i.e. found out that it is invalid) a goal of a tree t′′ with (j, (Π, t′′)) ∈ F. Then we should backtrack up to an “unsafe” step that may have caused this invalidity. In case of safeness, we know that Π is invalid.

• If there have been no Instantiation steps affecting the sequent Π, then we should remove (j, (Π, t′′)) from the proof forest F and undo all its applications as a lemma, i.e. the Expansion steps of Def. 4.9 where j occurs in the set N.

• Otherwise, we undo an Instantiation step affecting the sequent Π, and then see whether we can still detect a failure by again disproving the disinstantiated goal.

Definition 4.11 (Safeness Invariant Condition) The safeness invariant condition on (F, ∅, R, L) is that, for all (i, (Γ, t)) ∈ F,

Goals({t}) R-reduces to {Γ }.

Definition 4.12 (Safeness of Expansion Steps and Sub-rules) An Expansion step of the sequent calculus of Def. 4.9 is safe if G R′-reduces to {Δ}. A sub-rule of the Expansion rule of the sequent calculus of Def. 4.9 is safe if it describes only safe Expansion steps.

Theorem 4.13 (Safeness) The above safeness invariant condition is always satisfied for the tableau calculus of Def. 4.9. The above safeness invariant condition is always satisfied for the sequent calculus of Def. 4.9 if all Expansion steps are safe.

4.4 Concrete Sequent and Tableau Calculus

The examples of α-, β-, γ-, δ-, and Rewrite-rules of Section 1.2 can be modeled as safe Expansion steps as follows: Let

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

denote a sub-rule of the Expansion rule of the sequent calculus of Def. 4.9 which is given by N := ∅ (i.e. no lemmas are applied), G := {Π_{0}, …, Π_{n−1}}, and R′ := R ∪ R′′. For R′′ = ∅, the ‘R′′’ to the right of the bar is omitted.

For such a rule really being a safe sub-rule of the Expansion rule we have to show that {Δ} R′-reduces to G and vice versa, namely that G R′-reduces to {Δ}. By Lemma 4.4(5b) and because R does not matter here, it suffices to actually show that {Δ} R′′-reduces to G and vice versa.

Theorem 4.14 The examples of α-, β-, γ-, δ-, and Rewrite-rules of Section 1.2 are safe sub-rules of the Expansion rule of the sequent calculus of Def. 4.9.

Note that the resp. rules for the tableau calculus of Def. 4.9 differ only in G consisting simply of the set of the first formulas of the sequents below the bar.

Moreover, note that the R′′ of the δ-rule simplifies to V_{∃}(A, Γ Π) × {x^{∀,w}} in our weak version here because (as strong free universal variables are treated just like weak ones) we can always assume all occurring free universal variables to be weak ones.

Now we will present one simple rule for applying Π instantiated with a substitution ϱ as a lemma to expand a goal Δ of a proof tree t. We will formulate this as an Expansion step in the tableau calculus of Def. 4.9 (sequent calculus analogously) as follows.

Theorem 4.15 The following describes a sub-rule of the Expansion rule of the tableau calculus of Def. 4.9: Let (F, ∅, R, L) be a proof forest. Let (i, (Γ, t)), (j, (Π, t′)) ∈ F. Let R′ be a variable-condi-tion with R⊆R′. Let l be an arbitrary leaf of t. Set N := {j}. Assume L^{∗} ∩ ({i}×N) = ∅. Set Y := { y^{∀,w} ∈ V_{∀,w}(Π) | V_{∃}(Π)×{y^{∀,w}} ⊆ R′ }. Let ϱ ∈ Y → (V_{∃}\V_{∃}(F)) be an injective substitution. Set G to be the set containing the sequents \overline{Bϱ} for each formula B listed in the sequent Π.

Note that Y contains exactly those free universal variables of Π that have no free existential variables in their scopes when imagining any list of quantifiers for all free variables of Π that represents (a superset of) R′. In other words, the variables in Y are those weak free universal variables on that no solution for the free existential variables in Π depends. Therefore, the variables in Y are those which we can instantiate when applying the lemma Π. Although it does not seem impossible to instantiate more variables for a lemma application, this does not seem to be necessary, especially because we can extend the variable-condition with V_{∃}(Π)×{y^{∀,w}} in order to instantiate y^{∀,w} when applying the lemma.

Example 4.16 (Tableaux Proof in Group Theory) Assume that in the signature Σ we have the operator ∗, the constant 1, and the inverse function inv. We start with the empty proof forest (∅, ∅, ∅, ∅). We start the new proof tree number 1 for

x_{1}^{∀,w} ∗ (y_{1}^{∀,w} ∗ z_{1}^{∀,w}) = (x_{1}^{∀,w} ∗ y_{1}^{∀,w}) ∗ z_{1}^{∀,w}

by a Hypothesizing step in the tableau calculus of Def. 4.9. We start the new proof tree number 2 for

1 ∗ x_{2}^{∀,w} = x_{2}^{∀,w}

by a Hypothesizing step. We start the new proof tree number 3 for

inv(x_{3}^{∀,w}) ∗ x_{3}^{∀,w} = 1

by a Hypothesizing step. With these three trees we have the axioms of group theory at hand via lemma application. Now we really want to prove something. We start the new proof tree number 4 for

∀x: x ∗ inv(x) = 1

by a Hypothesizing step. The the root of proof tree 4 is labeled with

¬∀x: x ∗ inv(x) = 1

Note that all proof trees in this example will have branching degree 1. A δ-step (cf. Theor. 4.14) adds the child

x_{4}^{∀,w} ∗ inv(x_{4}^{∀,w}) ≠ 1

Our variable-condition is still empty because no free variables occur in x ∗ inv(x) = 1. Applying the sequent of proof tree 3 in the way of Theor. 4.15 adds the new child

inv(x1^{∃}) ∗ x1^{∃} = 1

to proof tree 4 and inserts the pair (3, 4) to our lemma application relation. A Rewrite step (cf. Theor. 4.14) with this equality from right to left produces the new child

x_{4}^{∀,w} ∗ inv(x_{4}^{∀,w}) ≠ inv(x1^{∃}) ∗ x1^{∃}

Applying the sequent of proof tree 2 in the way of Theor. 4.15 adds the new child

1 ∗ x2^{∃} = x2^{∃}

to proof tree 4 and inserts the pair (2, 4) to our lemma application relation. An Instantiation step (cf. Def. 4.9) transforms this child into

1 ∗ x1^{∃} = x1^{∃}

which can be used for a Rewrite step form right to left adding the child

x_{4}^{∀,w} ∗ inv(x_{4}^{∀,w}) ≠ inv(x1^{∃}) ∗ (1 ∗ x1^{∃})

Applying the sequent of proof tree 3 in the way of Theor. 4.15 adds the new child

inv(x3^{∃}) ∗ x3^{∃} = 1

A Rewrite step (cf. Theor. 4.14) with this equality from right to left produces the new child

x_{4}^{∀,w} ∗ inv(x_{4}^{∀,w}) ≠ inv(x1^{∃}) ∗ ((inv(x3^{∃}) ∗ x3^{∃}) ∗ x1^{∃})

With two applications of the sequent of proof tree 1, this can be rewritten into

x_{4}^{∀,w} ∗ inv(x_{4}^{∀,w}) ≠ (inv(x1^{∃}) ∗ inv(x3^{∃})) ∗ (x3^{∃} ∗ x1^{∃})

Note that our lemma application relation now is {1, 2, 3} × {4}. Applying the sequent of proof tree 3 in the way of Theor. 4.15 adds the new child

inv(x4^{∃}) ∗ x4^{∃} = 1

In order to use this for a Rewrite step from left to right we apply the unifier σ := {x1^{∃}↦inv(x3^{∃}), x4^{∃}↦inv(x3^{∃})} to the whole proof forest and get the new child

x_{4}^{∀,w} ∗ inv(x_{4}^{∀,w}) ≠ 1 ∗ (x3^{∃} ∗ inv(x3^{∃}))

Note that this unifier is an existential ∅-substitution and that the σ-update of our variablecondition ∅ is still the empty variable-condition ∅. With an application of the sequent of proof tree 2, this can be rewritten into

x_{4}^{∀,w} ∗ inv(x_{4}^{∀,w}) ≠ x3^{∃} ∗ inv(x3^{∃})

An instantiation step produces the new child

x_{4}^{∀,w} ∗ inv(x_{4}^{∀,w}) ≠ x_{4}^{∀,w} ∗ inv(x_{4}^{∀,w})

Now the tree is closed because all sequents of the form (t = t) Λ are assumed to be in our axioms AX. By Theor. 4.8 we now know that ∀x: x ∗ inv(x) = 1 is ∅-valid, provided that the proof trees 1, 2, and 3 are closed, which is the case when we assume their sequents to be in AX.

Now we start proof tree 5 for

x_{5}^{∀,w} ∗ inv(x_{5}^{∀,w}) = 1

by a Hypothesizing step. Note that the sequent is not really different from that of proof tree 4. In order to have only one version of each lemma we should generally decide on one form of the sequents. We do prefer the form of proof tree 5 because it will be more useful for inductive theorem proving. For deductive theorem proving, the two only differ in that the form of proof tree 5 is handier for lemma application. To see this, we will prove each with the help of the other. A lemma application according to Theor. 4.15 of the sequent of proof tree 4 to proof tree 5 whose root is labeled with

x_{5}^{∀,w} ∗ inv(x_{5}^{∀,w}) ≠ 1

adds the child

∀x: x ∗ inv(x) = 1

A γ-step adds the child

x5^{∃} ∗ inv(x5^{∃}) = 1

An Instantiation step transforms this into

x_{5}^{∀,w} ∗ inv(x_{5}^{∀,w}) = 1

Now proof tree 5 is closed because all sequents of the form A Λ \overline{A} are assumed to be in our axioms AX. Finally, we start another proof tree number 6 for the sequent of proof tree 4. The root is again labeled with

¬∀x: x ∗ inv(x) = 1

A δ-step adds the child

x_{6}^{∀,w} ∗ inv(x_{6}^{∀,w}) ≠ 1

Applying the sequent of proof tree 5 in the way of Theor. 4.15 adds the new child

x6^{∃} ∗ inv(x6^{∃}) = 1

An Instantiation step transforms this into

x_{6}^{∀,w} ∗ inv(x_{6}^{∀,w}) = 1

Now proof tree 6 is also closed because all sequents of the form A \overline{A} Λ are assumed to be in our axioms AX.

5 The Strong Version

5.1 Why is it so difficult?

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, these additional solutions pose some problems because they may tear some strong free universal variables out of their contexts:

Example 5.1 (Reduction & Liberalized δ-Steps)

In Ex. 1.3 a liberalized δ-step reduced

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

to

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

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^{∀,s}).

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^{∀,s}) := 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 I 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 existential R-substitution {x^{∃}↦y^{∀,s}} transforms the reduction of Ex. 5.1 into the reduction of

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

to

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

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 under 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 I 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^{∀,s}} → A such that the former sequent is (_{V_{∀}\{y^{∀,s}}}|π⊎η, e, A)-valid instead of (π, e, A)-valid. Choosing η := {y^{∀,s}↦a} would solve the problem of Ex. 5.1 then: Indeed, the former sequent is (_{V_{∀}\{y^{∀,s}}}|π⊎η, e, A)-valid because for the e of Ex. 5.1 we have e(x^{∃})(_{V_{∀}\{y^{∀,s}}}|π⊎η) = (_{V_{∀}\{y^{∀,s}}}|π⊎η)(y^{∀,s}) = 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 strong free universal variable, say z^{∀,s}, occurs in the principal formula, as, e.g., in the reduction of

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

to

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

In this case, for the e of Ex. 5.1 (which gives x^{∃} the value of y^{∀,s}) the η ∈ {y^{∀,s}} → A must change when the π-value of z^{∀,s} changes:

E.g., for π := {y^{∀,s}↦a, z^{∀,s}↦b} we need η(y^{∀,s}) := b,
while for π := {y^{∀,s}↦b, z^{∀,s}↦a} we need η(y^{∀,s}) := a.

Indeed, in the reduction above, y^{∀,s} is functionally dependent on z^{∀,s}. This dependency is the main^{10} reason for our new requirement on our liberalized δ-rule, namely to insert (z^{∀,s}, y^{∀,s}) into the variable-condition.

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

Thus, the only solution can be that η depends on some values of π but 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 strong free universal variables introduced by liberalized δ-steps really play. And this is what the choice-conditions of the following section are about.

After all the above-mentioned changes, our notion of “strong reduction” has proven to be appropriate. It is still the same today as it was in Wirth (1998a) and Wirth (1998b). Contrariwise, the notion of “strong validity” had to be changed, in order to make lemma application possible. Namely, we had to replace an “all” in Def. 5.7 with a “some”. The little change required completely new proofs, but the lemmas and theorems hardly changed. The notion of “strong validity” now goes together better with the notion of “strong reduction” in the sense that both the e and the π are existentially quantified in the notion of “strong validity” and both the e and the π are universally quantified in the notion of “strong reduction”.

5.2 Choice-Conditions

Definition 5.2 (Choice-Condition, Extension) C is an R-choice-condition if C is a (possibly) partial function from V_{∀,s} into the set of formulas, R is a variable-condition, R^{+} is a wellfounded ordering on V_{free}, and, for all y^{∀,s} ∈ dom(C):

z R^{+} y^{∀,s} for all z ∈ V_{free}(C(y^{∀,s}))\{y^{∀,s}}.

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

Note that the empty function ∅ is an R-choice-condition for any variable-condition R for that R^{+} is a wellfounded ordering, which in the following will always be the case.

Definition 5.3 (Compatibility) Let C be an R-choice-condition, A a Σ-structure, and e a strong existential (A, R)-valua-tion. π is (e, A)-compatible with (C, R) if

1. π ∈ V_{∀,s} → ((V_{∀,w} ⇝ A) ⇝ A) is semantic and (R ∪ S_{e} ∪ S_{π})^{+} is a wellfounded ordering, cf. Def. 3.5.

2. For all τ ∈ V_{∀,w} → A and y^{∀,s} ∈ dom(C):

If C(y^{∀,s}) is (ϵ(π)(τ) ⊎ τ, e, A)-valid,

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

Item 1 of this definition is quite technical and needed for lemma application. Roughly speaking, it says that the information flow between variables expressed in R, e, and π is acyclic.

Item 2 of (e, A)-compatibility of π with ({(y^{∀,s}, B)}, R) means that a different choice for the ϵ(π)(τ)-value of y^{∀,s} does not destroy the validity of the formula B in

A ⊎ ϵ(e)(ϵ(π)(τ) ⊎ τ) ⊎ ϵ(π)(τ) ⊎ τ,

or that ϵ(π)(τ)(y^{∀,s}) is chosen such that B becomes invalid if such a choice is possible. This is closely related to Hilbert’s ε-operator (cf. Hilbert & Bernays (1968/70), Vol. II) in the sense that y^{∀,s} is given the value of εy: (¬B{y^{∀,s}↦y}) for y ∈ V_{bound}\V(B). Since the choice for y^{∀,s} depends on the other free variables of B (i.e. the free variables of εy: (¬B{y^{∀,s}↦y}) ), we required the inclusion of this dependency into the transitive closure of the variable-con-dition R in Def. 5.2.

Lemma 5.4 Let C be an R-choice-condition, A a Σ-structure, and e a strong existential (A, R)-valua-tion. Now, there is some π that is (e, A)-compatible with (C, R).

Definition 5.5 (Extended σ-Update) Let C be an R-choice-condition and σ a strong existential R-substitution. The extended σ-update (C′, R′) of (C, R) is given by

C′ := { (x, Bσ) | (x, B) ∈ C }, R′ is the strong σ-update of R.

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

5.3 Strong Validity

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

Definition 5.7 (Strong Validity)

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

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

G is (C, R)-strongly (e, A)-valid if G is strongly (π, e, A)-valid for some^{11} π that is (e, A)- compatible with (C, R).

G is strongly (π, e, A)-valid if G is (ϵ(π)(τ) ⊎ τ, e, A)-valid for each τ ∈ V_{∀,w} → A.

The rest is given by Def. 4.1.

Note that strong validity is called “strong” because it treats the strong free universal variables properly, whereas weak validity does not. It is generally not the case, however, that strong validity is logically stronger than weak validity. The logical strength of the two cannot be easily compared, but we do not need to know more than the following two lemmas.

Lemma 5.8 (From Weak to Strong Validity) Let C be an R-choice-condition, A a Σ-structure, and G a set of sequents. Now: If G is V_{∃}×V_{∀}-valid in A, then G is (C, R)-strongly valid in A.

On the other hand, from (C, R)-strong validity of a set of sequents G we should be able to infer (∅, R′)-strong validity and (weak) R′-validity (which implies ∅-validity, cf. Lemma 4.4(5a)) for some G with the strong free universal variables renamed to some new free existential variables.

Lemma 5.9 (From Strong to Weak Validity) Let C be an R-choice-condition, A a Σ-structure, and G a set of sequents. Let ς: V_{∀,s}(G) → (V_{∃}\V(G)) be injective. If G is (C, R)-strongly valid in A, then Gς is (∅, R′)-strongly valid and (weakly) R′-valid in A for

R′ := (_{V_{∀,w}∪V_{∃}\ran(ς)}|id ⊎ ς^{−1}) ∘ R^{+}|_{V_{∀,w}∪V_{∃}\ran(ς)} ⊎ V_{∃}×V_{∀,s}.

5.4 Strong Reduction

Definition 5.10 (Strong Reduction) Let C be an R-choice-condition, A a Σ-structure, and G_{0}, G_{1} sets of sequents. G_{0} (C, R)-strongly reduces to G_{1} in A if for each strong existential (A, R)-valuation e and each π that is (e, A)-compatible with (C, R):

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

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_{∀,s} → ((V_{∀,w} ⇝ A) ⇝ A)) …:

( G_{1} strongly (π, e, A)-valid ⇒ G_{0} strongly (π, e, A)-valid ).

This fundamental difference in the nature of reduction cannot be removed.^{12}

Lemma 5.11 (Strong Reduction) Let C be an R-choice-condition; A a Σ-structure; G_{0}, G_{1}, G_{2}, and G_{3} sets of sequents.

1. (Validity)

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

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

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

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

4. (Additivity)

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

5. (Monotonicity) For (C′, R′) being an extension of (C, R):

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

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

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

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

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

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

5.5 Abstract Sequent and Tableau Calculus

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.12 (Strong Proof Forest) A strong (deductive) proof forest in a sequent (or else: tableau) calculus is a quadruple (F, C, R, L) where C is an R-choice-condition, L ⊆ IN_{+}×IN_{+}, and F is a partial function from IN_{+} into the 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.6 are not changed. Note, however, that the V_{∃}×V_{∀}-validity of AX implies (C, R)-strong validity of AX for any R-choice-condition C, cf. Lemma 5.8.

Definition 5.13 (Strong Soundness Invariant Condition) The strong soundness invariant condition on (F, C, R, L) is that, for all (i, (Γ, t)) ∈ F,

{Γ } (C, R)-strongly reduces to Goals({ t′ | (i′, (Γ′, t′)) ∈ F ∧ i′L^{∗}i }).

Theorem 5.14 (Successful Proof) Let the strong proof forest (F, C, R, L) satisfy the above strong soundness invariant condition. Let (i, (Γ, t)) ∈ F. Suppose that all trees in { t′ | (i′, (Γ′, t′)) ∈ F ∧ i′L^{∗}i } are closed. Now: Γ is (C, R)-strongly valid and, for any injective ς: V_{∀,s}(Γ) → (V_{∃}\V(Γ)), Γ ς is (∅, R′)-strongly valid and (weakly) R′-valid for R′ := (_{V_{∀,w}∪V_{∃}\ran(ς)}|id ⊎ ς^{−1}) ∘ R^{+}|_{V_{∀,w}∪V_{∃}\ran(ς)} ⊎ V_{∃}×V_{∀,s}.

Definition 5.15 (Abstract Sequent (or else: Tableau) Calculus)

We start with the empty strong proof forest (F, C, R, L) := (∅, ∅, ∅, ∅) and then iterate only the following kinds of modifications of (F, C, R, L) (resulting in (F′, C′, R′, L′)):

Hypothesizing: Either, set C′ := C and R′ := R∪R′′ for some variable-condition R′′ with ran(R′′)∩dom(R′) = ∅, or, more generally, let (C′, R′) be an extension of (C, R). Set L′ := L. Let i ∈ IN_{+} \ dom(F). 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 ∪ {(i, (Γ, t))}.

Expansion: Let (i, (Γ, t)) ∈ F. Let (C′, R′) be an extension of (C, R). Let N ⊆ dom(F) such that L^{∗} ∩ ({i}×N) = ∅. 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 (C′, R′)-reduces to G ∪ dom(⟨N⟩F) (or else: { ΛΔ | Λ ∈ G } ∪ dom(⟨N⟩F)), then we may set L′ := L ∪ N×{i} and F′ := (F \{(i, (Γ, t))}) ∪ {(i, (Γ, 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 σ-update of (C, R). Then we may set L′ := L and F′ := { (i, (Γ σ, tσ)) |

(i, (Γ, t)) ∈ F }.

Note that it is a good idea for a Hypothesizing step that the new sequent Γ gets fresh weak free universal variables, i.e. V_{∀,w}(Γ) ∩ V(F, C, R) = ∅. Moreover, requiring R′′ ⊆ V_{∃}×V_{∀,w}(Γ) does not seem to be restrictive in practice. In this important case the condition of ran(R′′)∩dom(R′) = ∅ is always satisfied and we therefore have mentioned it explicitly in the above formulation of the Hypothesizing step.

Theorem 5.16 (Soundness) The above strong soundness invariant condition is always satisfied for the sequent (or else: tableau) calculus of Def. 5.15.

Definition 5.17 (Strong Safeness Invariant Condition) The strong safeness invariant condition on (F, C, R, L) is that, for all (i, (Γ, t)) ∈ F,

Goals({t}) (C, R)-strongly reduces to {Γ }.

Definition 5.18 (Safeness of Expansion Steps and Sub-rules) An Expansion step of the sequent calculus of Def. 5.15 is safe if G (R′, C′)-strongly reduces to {Δ}. A sub-rule of the Expansion rule of the sequent calculus of Def. 5.15 is safe if it describes only safe Expansion steps.

Theorem 5.19 (Safeness) The above strong safeness invariant condition is always satisfied for the tableau calculus of Def. 5.15. The above strong safeness invariant condition is always satisfied for the sequent calculus of Def. 5.15 if all Expansion steps are safe.

5.6 Concrete Sequent and Tableau Calculus

The examples of α-, β-, γ-, δ- liberalized δ-, and Rewrite-rules of Section 1.2 can be modeled as safe Expansion steps as follows: Let

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

denote a sub-rule of the Expansion rule of the sequent calculus of Def. 5.15 which is given by N := ∅ (i.e. no lemmas are applied), G := {Π_{0}, …, Π_{n−1}}, C′ := C ∪ C′′, and R′ := R ∪ R′′. For C′′ = R′′ = ∅, the ‘C′′’ and ‘R′′’ to the right of the bar are omitted.

For such a rule really being a safe sub-rule of the Expansion rule we have to show that C′ is an R′-choice-condition and that {Δ} strongly (C′, R′)-reduces to G and vice versa, namely that G strongly (C′, R′)-reduces to {Δ}.

Theorem 5.20 The examples of α-, β-, γ-, δ-,^{13} liberalized δ-, and Rewrite-rules of Section 1.2 are safe sub-rules of the Expansion rule of the sequent calculus of Def. 5.15.

The following example shows that R′′ of the liberalized δ-rule of Section 1.2 must indeed contain V_{∀}(A) × {x^{∀,s}} and that the transitive closure over R′ must be considered for the property of being a strong existential R′-substitution.

Example 5.21

∃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) ), ∃y: ∀x: ( ¬Q(x, y) ∨ ∀z: Q(x, z) )

Liberalized δ-step:

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

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

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

Liberalized δ-step:

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

with additional choice-condition (z^{∀,s}, Q(x^{∀,s}, z^{∀,s})) and additional variable-condition (x^{∀,s}, z^{∀,s}), i.e. the current variable-condition R′ is given by

\begin{matrix}y^{∃} & \overline{_{_{R} >}} & x^{∀,s} \\ z^{∀,s} & ^{∨^{R′′}} \end{matrix}

Note that now we have y^{∃}R′^{+}z^{∀,s} although y^{∃} does not appear in Q(x^{∀,s}, z).

Thus, both the inclusion of the free universal variables of the principle formula into the domain of the variable-condition and the transitive closure over it are necessary for σ := {y^{∃}↦z^{∀,s}} not being a strong existential R′-substitution in our state of proof. The latter fact is, however, essential for soundness, because without it we could complete the proof attempt by application of σ in an Instantiation step, leading to the tautology

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

Now we will present one simple rule for applying Π instantiated with a substitution ϱ as a lemma to expand a goal Δ of a proof tree t. We will formulate this as an Expansion step in the tableau calculus of Def. 5.15 (sequent calculus analogously) as follows.

Theorem 5.22 The following describes a sub-rule of the Expansion rule of the tableau calculus of Def. 5.15: Let (F, C, R, L) be a strong proof forest. Let (i, (Γ, t)), (j, (Π, t′)) ∈ F. Either, set C′:=C and let R′ be a variable-condition with R⊆R′ such that R′^{+} is a wellfounded ordering or, more generally, let (C′, R′) be an extension of (C, R). Let l be an arbitrary leaf of t. Set N := {j}. Assume L^{∗} ∩ ({i}×N) = ∅. Set

Y := { y^{∀,w} ∈ V_{∀,w}(Π) ( V_{∃}(Π) ∪ V_{∀,s}(Π) ) × {y^{∀,w}} ⊆ R′ }.

Let ϱ ∈ Y → (V_{∃}\V(F, C, R, L)) be an injective substitution. Set G to be the set containing the sequents \overline{Bϱ} for each formula B listed in the sequent Π.

Note that Y contains exactly those free universal variables of Π that have neither free existential variables nor strong free universal variables of Π in their scopes when imagining any list of quantifiers for all free variables of Π that represents (a superset of) R′. In other words, the variables in Y are those weak free universal variables on that neither a solution for the free existential variables nor a choice-condition for the strong free universal variables in Π depends. Therefore, the variables in Y are those which we can instantiate when applying the lemma Π. Although it does not seem impossible to instantiate more variables for a lemma application, this does not seem to be necessary, especially because we can extend R′ with ( V_{∃}(Π) ∪ V_{∀,s}(Π) ) × {y^{∀,w}} in order to instantiate y^{∀,w} when applying the lemma, provided that R′^{+} is still a wellfounded ordering.

Moreover, note that (as far as Theor. 5.20 and Theor. 5.22 are concerned) the choiceconditions do not have any influence on our proofs when, in the liberalized δ-steps, we always choose a completely new strong free universal variable x^{∀,s} that does not occur elsewhere. Thus, the choice-conditions may be omitted in an implementation. 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 (weak) V_{∃}×V_{∀}-validity of AX, (C, R)-strong validity of AX (which is logically weaker, cf. Lemma 5.8) is sufficient for Theor. 5.14.

2. If we add a functional behavior to a choice-condition C, i.e. if we require that for (x^{∀,s}, A) ∈ C the value for x^{∀,s} 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 strong free universal variable for the same C-value and by later equating strong 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.23

Starting with the empty proof tree and hypothesizing

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

with the rules of Section 1.2 we can produce a proof tree with the leaves

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

and

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

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

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

Note that if we had applied the δ-rule instead of the liberalized δ-rule in the above proof, i.e. if we had introduced x^{∀,w} instead of x^{∀,s}, then we would not only be unable to provide any information on our query variable (because the choice-condition is empty), but we would even be unable to finish our proof because due to the new variable-condition R = (z^{∃}, x^{∀,w}) we cannot apply {y^{∃}↦x^{∀,w}, z^{∃}↦x^{∀,w}} anymore, because it is not a strong existential R-substitution anymore. It is not even a (weak) existential R-substitution anymore. Thus, even with our weak version of Section 4 we could not complete the proof. With the (weak) δ-rule, all we can show is

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

instead.

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

All in all, when interested in theorem proving only, the (compared to the weak version) additional choice-condition of the strong version does not produce any overhead because it can simply be omitted. This is interesting because choice-conditions or Hilbert’s ε-terms 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.20 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 circularitycheck which can be done on a 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↦x_{A}^{∀,s}}, B{x↦x_{B}^{∀,s}}, the variable-conditions introduced for x_{A}^{∀,s} and x_{B}^{∀,s} may be smaller than the variable-condition introduced for y^{∀,s} after applying these rules to ∀x: (A∨B), resulting in A{x↦y^{∀,s}}, B{x↦y^{∀,s}}, i.e. R⟨{x_{A}^{∀,s}}⟩ and R⟨{x_{B}^{∀,s}}⟩ may be proper subsets of R⟨{y^{∀,s}}⟩. 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↦x_{A}^{∀,s}}, B{x↦x_{B}^{∀,s}} in parallel and may later decide to prove the stronger A{x↦y^{∀,s}}, B{x↦y^{∀,s}} instead, simply by merging the nodes for x_{A}^{∀,s} and x_{B}^{∀,s} and substituting x_{A}^{∀,s} and x_{B}^{∀,s} with y^{∀,s}.

6 Conclusion and Outlook

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. In the present version, lemma application is included for the first time in all our calculi. Induction hypothesis application will be included into future versions.

To our knowledge^{14} 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.

The Proofs

Proof of Lemma 3.8

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

\underline{\underline{(2):}} Here we denote concatenation (product) of relations ‘∘’ simply by juxtaposition and assume it to have higher priority than any other binary operator. Set σ′ := _{V_{∃}\dom(σ)}|id ∪ σ. Let e′ be some [strong] existential (A, R′)-valuation. Define S_{e} := S_{e′}(_{V_{∃}\dom(σ)}|id ∪ 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 (R ∪ S_{e})^{+} 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) ∈_{V_{∃}\dom(σ)}|id ∪ 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′}(_{V_{∃}\dom(σ)}|id ∪ E_{σ})R ∪ U_{σ}R and U_{σ}R is irreflexive (as σ is an existential R-substitution), it suffices to show irreflexivity of S_{e′}(_{V_{∃}\dom(σ)}|id ∪ E_{σ})R. Since R′ is the σ-update of R, this is a subset of S_{e′}R′, which is irreflexive because e′ is an existential (A, R′)-valuation. \underline{Q.e.d. (Claim 3)} \underline{Proof of Claim 4:} (R′ ∪ S_{e′})^{+} is a wellfounded ordering because e′ is a strong existential (A, R′)-valuation. Moreover, as R′ is the strong σ-update of R, we have^{15} R′ = R ∪ E_{σ} ∪ U_{σ}. Thus, (R ∪ E_{σ} ∪ U_{σ} ∪ S_{e′})^{+} is a wellfounded ordering, just like its subset (R ∪ S_{e′}(_{V_{∃}\dom(σ)}|id ∪ E_{σ}) ∪ U_{σ})^{+}, which is equal to (R ∪ S_{e})^{+}. \underline{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.8)

Proof of Lemma 4.4 (1), (2), (3), and (4) are trivial. Note that (5) is a trivial consequence of Lemma 3.8(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.8(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.8(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.4)

Proof of Theor. 4.8 Since AX is V_{∃}×V_{∀}-valid and R ⊆ V_{∃}×V_{∀}, by Lemma 4.4(5a), AX is R-valid. Set T := { t′ | (i′, (Γ′, t′)) ∈ F ∧ i′L^{∗}i }. Since all trees in T are closed, we have Goals(T) ⊆ AX . Thus, Goals(T) is R-valid. Since (i, (Γ, t)) ∈ F and (F, ∅, R, L) satisfies the soundness invariant condition, {Γ } R-reduces to Goals(T). All in all, by Lemma 4.4(1), Γ is R-valid.

Q.e.d. (Theor. 4.8)

Proof of Theor. 4.10

(∅, ∅, ∅, ∅) trivially satisfies the soundness invariant condition.

For the iteration steps, we let (i′′, (Γ′′, t′′)) ∈ F′ be arbitrary and set

T (i) := { t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F′ ∧ i′′′L′^{∗}i }.

Assuming the soundness invariant condition for (F, ∅, R, L), we have to show that {Γ′′} R′-reduces to Goals(T (i′′)).

Hypothesizing: Note that F′ is a partial function on IN_{+} just like F because of i ∈ IN_{+} \ dom(F). \underline{(i′′, (Γ′′, t′′)) ∈ F:}

{Γ′′} R-reduces to Goals({ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ })

by assumption, and then, due to R⊆R′ and Lemma 4.4(5),

{Γ′′} R′-reduces to Goals({ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ }).

Thus, by Lemma 4.4(2,3), we only have to show { t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ } ⊆ T (i′′). But this follows from L = L′ and F ⊆F′. \underline{(i′′, (Γ′′, t′′)) = (i, (Γ, t)):} Then \{Γ′′\} = \{Γ \} = Goals(\{t\}) = Goals(\{t′′\}) ⊆ Goals(T (i′′)). Thus, by Lemma 4.4(2), {Γ′′} R′-reduces to Goals(T (i′′)).

\underline{\underline{Expansion:}} \underline{Claim 1:} For n ∈ N, (Π, t′′′′) = F (n): \{Π\} R′-reduces to Goals(T (i)). \underline{Proof of Claim 1:} \{Π\} R-reduces to Goals(\{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}n \}) by assumption. Thus, by R⊆R′ and Lemma 4.4(5),

{Π} R′-reduces to Goals({ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}n }).

Since L^{∗} ∩ ({i}×N) = ∅, _{IN_{+}\{i}}|F′ =_{IN_{+}\{i}}|F , and L′ = L ∪ N×{i}, we have

\begin{aligned}\{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}n \} & = \\ \{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}n ∧ i′′′ ≠ i \} & ⊆ \\ \{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F′ ∧ i′′′L^{∗}n \} & ⊆ \\ \{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F′ ∧ i′′′L′^{∗}i \} & = T (i). \end{aligned}

Thus, by Lemma 4.4(2,3), \{Π\} R′-reduces to Goals(T (i)). \underline{Q.e.d. (Claim 1)} \underline{Claim 2:} Goals(\{t\}) R′-reduces to Goals(T (i)). \underline{Proof of Claim 2:} As Goals(\{t\})\\{Δ\} ⊆ Goals(\{t′\}) ⊆ Goals(\{t′\}) ∪ dom(⟨N⟩F), by Lemma 4.4(2),

Goals({t})\{Δ} R′-reduces to Goals({t′}) ∪ dom(⟨N⟩F).

Thus, since by assumption {Δ} R′-reduces to a subset of Goals({t′}) ∪ dom(⟨N⟩F), by Lemma 4.4(4),

Goals({t}) R′-reduces to Goals({t′}) ∪ dom(⟨N⟩F).

Moreover, since {t′} ⊆ T (i), by Lemma 4.4(2), Goals({t′}) R′-reduces to Goals(T (i)). Thus, by Claim 1 and Lemma 4.4(4)

Goals({t′}) ∪ dom(⟨N⟩F) R′-reduces to Goals(T (i)).

Thus, by Lemma 4.4(3), Goals(\{t\}) R′-reduces to Goals(T (i)). \underline{Q.e.d. (Claim 2)}

By assumption {Γ′′} R-reduces to Goals({ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ }). Thus, by R⊆R′ and Lemma 4.4(5),

{Γ′′} R′-reduces to Goals({ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ }).

\underline{(i, i′′) ∉ L^{∗}:} Since _{IN_{+}\\{i\}}|F′ =_{IN_{+}\\{i\}}|F , L⊆L′ we have

\begin{aligned}\{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ \} & = \\ \{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ ∧ i′′′ ≠ i \} & ⊆ \\ \{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F′ ∧ i′′′L^{∗}i′′ \} & ⊆ \\ \{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F′ ∧ i′′′L′^{∗}i′′ \} & = T (i′′). \end{aligned}

Thus, by Lemma 4.4(2),

Goals({ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ }) R′-reduces to Goals(T (i′′)).

Thus, by Lemma 4.4(3), {Γ′′} R′-reduces to Goals(T (i′′)).

\underline{(i, i′′) ∈ L^{∗}:} Since _{IN_{+}\\{i\}}|F′ =_{IN_{+}\\{i\}}|F , L⊆L′ we have

\begin{aligned}\{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ \} & = \\ \{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ ∧ i′′′ ≠ i \} ∪ \{t\} & ⊆ \\ \{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F′ ∧ i′′′L^{∗}i′′ \} ∪ \{t\} & ⊆ \\ \{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F′ ∧ i′′′L′^{∗}i′′ \} ∪ \{t\} & = T (i′′) ∪ \{t\}. \end{aligned}

Thus, by Lemma 4.4(2,3),

{Γ′′} R′-reduces to Goals(T (i′′)) ∪ Goals({t}).

By Lemma 4.4(2), Goals(T (i′′)) R′-reduces to Goals(T (i′′)). Thus, by Claim 2 and Lemma 4.4(4), Goals(T (i′′)) ∪ Goals({t}) R′-reduces to Goals(T (i′′)) ∪ Goals(T (i)) = Goals(T (i′′)). The latter equality holds because we have T (i) ⊆ T (i′′) here. Finally, by Lemma 4.4(3), {Γ′′} R′-reduces to Goals(T (i′′)).

\underline{\underline{Instantiation:}} Set (Γ, t) := F (i′′). Then Γ′′ = Γ σ. By assumption,

{Γ } R-reduces to Goals({ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ }).

By Lemma 4.4(6b), {Γ′′} R′-reduces to Goals({ t′′′σ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ }) = Goals({ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F′ ∧ i′′′L^{∗}i′′ }) = Goals(T (i′′)).

Q.e.d. (Theor. 4.10)

Proof of Theor. 4.13

The empty proof forest trivially satisfies the safeness invariant condition.

\underline{\underline{Hypothesizing:}} When we assume the old trees from F to satisfy the safeness invariant condition for R, then they also satisfy it for R′ by Lemma 4.4(5b). The new tree (i, (Γ, t)) satisfies the safeness invariant condition because Goals({t}) = {Γ } and {Γ } R′-reduces to {Γ } by Lemma 4.4(2).

\underline{\underline{Expansion:}} When we assume the non-expanded trees to satisfy the safeness invariant condition for R, then they also satisfy it for R′ by Lemma 4.4(5b). For the new tree (i, (Γ, t′)) we have to show that Goals({t′}) R′-reduces to {Γ }. \underline{Claim 1:} Goals(\{t′\}) R′-reduces to Goals(\{t\}). \underline{Proof of Claim 1:} In case of the tableau calculus,

{ ΛΔ | Λ ∈ G } R′-reduces to {Δ}

because (e, A)-validity of Δ implies (e, A)-validity of ΛΔ. Moreover,

Goals({t′}) \ { ΛΔ | Λ ∈ G } R′-reduces to Goals({t})

by Lemma 4.4(2) due to Goals({t′}) \ { ΛΔ | Λ ∈ G } ⊆ Goals({t}). Thus, the claim follows by Lemma 4.4(4) due to Δ ∈ Goals({t}). In case of the sequent calculus, we have the additional requirement of safeness of the Expansion step, i.e.

G R′-reduces to {Δ}.

Moreover,

Goals({t′}) \ G R′-reduces to Goals({t})

by Lemma 4.4(2) due to Goals({t′}) \ G ⊆ Goals({t}). Thus, the claim follows by Lemma 4.4(4) due to Δ ∈ Goals(\{t\}). \underline{Q.e.d. (Claim 1)} When we assume the old tree (i, (Γ, t)) to satisfy the safeness invariant condition for R, then Goals({t}) R′-reduces to {Γ } by Lemma 4.4(5b). By Lemma 4.4(3), together with Claim 1 this implies that Goals({t′}) R′-reduces to {Γ }, as was to be shown.

\underline{\underline{Instantiation:}} By Lemma 4.4(6b).

Q.e.d. (Theor. 4.13)

Proof of Theor. 4.14

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

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

\underline{\underline{γ-rule:}} We have to show that

{Γ ∃x: A Π} ∅-reduces to {A{x↦x^{∃}} Γ ∃x: A Π}

in A and vice versa. This is the case, however, because (e, A)-validity of the two sets is logically equivalent for each existential (A, ∅)-valuation e. The implication from left to right is given because the former sequent is a sub-sequent of the latter. The other direction 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 rule 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.5), 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{\underline{δ-rule:}} Note that in this proof for soundness, we only make use of the weaker conditions on the occurrence of x^{∀,w} given by Note 2. By Lemma 4.4(5b) it suffices to show that

{Γ ∀x: A Π} R′′-reduces to {A{x↦x^{∀,w}} Γ Π}

in A for R′′ := V_{∃}(A, Γ Π) × {x^{∀,w}} and vice versa.

For the one direction, 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^{∀,w}}}|π′ = _{V_{∀}\{x^{∀,w}}}|π, simply because x^{∀,w} does not occur in Γ Π. Because of V_{∃}(Γ Π) × {x^{∀,w}} ⊆ R′′, we know that Γ Π must even be invalid in A ⊎ ϵ(e)(π′) ⊎ π′. Since the latter sequent is assumed to be (e, A)-valid, this means that A{x↦x^{∀,w}} is (π′, e, A)-valid. Because of V_{∃}(A{x↦x^{∀,w}}) × {x^{∀,w}} = V_{∃}(A) × {x^{∀,w}} ⊆ R′′, we know that A{x↦x^{∀,w}} must even be valid in A ⊎ ϵ(e)(π) ⊎ π′ for all π′ ∈ V_{∀} → A with _{V_{∀}\{x^{∀,w}}}|π′ = _{V_{∀}\{x^{∀,w}}}|π. 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.5), this means that ∀x:(A{x↦x^{∀,w}}{x^{∀,w}↦x}) is valid in A ⊎ ϵ(e)(π) ⊎ π. Since x^{∀,w} 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.

For the vice versa direction, it suffices to show that (π, e, A)-validity of ∀x:A implies (π, e, A)-validity of A{x↦x^{∀,w}}, which is trivial by the standard semantic definition of ∀.

\underline{\underline{Rewrite-rule:}} We have to show that

{Γ A[s] Π B Λ} ∅-reduces to {A[t] Γ Π B Λ}

in A and vice versa. This is the case, however, because (π, e, A)-validity of the two sets is logically equivalent for each existential (A, ∅)-valuation e and each π ∈ V_{∀} → A. If eval(A ⊎ ϵ(e)(π) ⊎ π)(s) ≠ eval(A ⊎ ϵ(e)(π) ⊎ π)(t), then both are (π, e, A)-valid because B is. Otherwise, we set a := eval(A ⊎ ϵ(e)(π) ⊎ π)(s), choose some for z^{∀} ∈ V_{∀}\V(A[s]), and define π′ ∈ V_{∀} → A by _{V_{∀}\{z^{∀}}}|π′ =_{V_{∀}\{z^{∀}}}|π and π′(z^{∀}) = a. Then a = eval(A ⊎ ϵ(e)(π) ⊎ π)(t). Moreover, by the Substitution-Lemma:

eval(A ⊎ ϵ(e)(π) ⊎ π)(A[s])  =
eval(A ⊎ ϵ(e)(π) ⊎ π)(A[z^{∀}]{z^{∀}↦s}) =
eval(A ⊎ ϵ(e)(π) ⊎ π′)(A[z^{∀}])  =
eval(A ⊎ ϵ(e)(π) ⊎ π)(A[z^{∀}]{z^{∀}↦t}) =
eval(A ⊎ ϵ(e)(π) ⊎ π)(A[t]).

Note that the usual problems with variables getting captured by quantifiers cannot occur in our context, because the formula (s≠t) cannot contain any variables from V_{bound} because it cannot contain any quantifiers and the unbound occurrence of variables from V_{bound} in formulas is not permitted, cf. Section 1.5.

Q.e.d. (Theor. 4.14)

Proof of Theor. 4.15 According to the definition of an Expansion step in the tableau calculus of Def. 4.9 we have to show that {Δ} R′-reduces to { AΔ | A ∈ G } ∪ {Π}. Thus, for A ∈ K, e an existential (A, R′)-valuation, it suffices to refute the assumption that { AΔ | A ∈ G }∪{Π} is (e, A)- valid, but Δ is not. Then there is some π ∈ V_{∀} → A such that Δ is not (π, e, A)-valid. Since all AΔ with A ∈ G must be (π, e, A)-valid, we know that G is (π, e, A)-valid. By the definition of G, this means that Πϱ is not (π, e, A)-valid. Define π′ ∈ V_{∀} → A by

π′(y) := ϵ(e)(π)(ϱ(y)) for y ∈ Y and π′(y) := π(y) for y ∈ V_{∀}\Y. \underline{Claim 1:} For x^{∃} ∈ V_{∃}(Π) we have ϵ(e)(π)(x^{∃}) = ϵ(e)(π′)(x^{∃}). \underline{Proof of Claim 1:} Otherwise there must be some y^{∀,w} ∈ Y with y^{∀,w} S_{e} x^{∃}. Since x^{∃} ∈ V_{∃}(Π) we have x^{∃} R′ y^{∀,w} by definition of Y. But then S_{e} ∘R′ is not irreflexive, which contradicts e being an existential (R′, A)-valuation. \underline{Q.e.d. (Claim 1)} The value of Π under eval(A ⊎ ϵ(e)(π′) ⊎ π′) is the same as the value of Π under eval(A ⊎ ϵ(e)(π) ⊎ π′) by Claim 1 which again is the same as the value of Πϱ under eval(A ⊎ ϵ(e)(π) ⊎ π) by the Substitution-Lemma. Thus, from Πϱ not being (π, e, A)-valid we know that Π is not (e, A)-valid, which is a contradiction. Q.e.d. (Theor. 4.15)

Proof of Lemma 5.4 Set ⊲ := (R ∪ S_{e})^{+} and S_{π} := ⊲ ∩ (V_{∀,w}×V_{∀,s}). As e is a strong existential (A, R)-valuation, ⊲ is a wellfounded ordering. With the help of a choice function and by noetherian induction on y^{∀,s} ∈ V_{∀,s} in ⊲ we can define π(y^{∀,s}): (S_{π}⟨{y^{∀,s}}⟩ → A) → A in the following way: Let τ ∈ S_{π}⟨{y^{∀,s}}⟩ → A. In case of y^{∀,s} ∈ V_{∀,s}\dom(C), we choose an arbitrary value for π(y^{∀,s})(τ) from the universe of A (of the appropriate sort). Note that universes are assumed to be non-empty. In case of y^{∀,s} ∈ dom(C), we choose a value for π(y^{∀,s})(τ) from the universe of A such that, if possible, C(y^{∀,s}) is not (ϵ(π)(τ ⊎ τ′) ⊎ τ ⊎ τ′, e, A)-valid for an arbitrary τ′ ∈ (V_{∀,w}\dom(τ)) → A.

\underline{Claim 1:} The definition of π(y^{∀,s})(τ) depends only on such π(v^{∀,s}) with v^{∀,s} ⊲ y^{∀,s}. \underline{Claim 2:} The definition of π(y^{∀,s})(τ) does not depend on τ′. \underline{Proof of Claim 1 and 2:} Since C is an R-choice-condition, we have z ⊲ y^{∀,s} for all z ∈ V_{free}(C(y^{∀,s}))\{y^{∀,s}}. Thus, for z^{∀,w} ∈ V_{∀,w}(C(y^{∀,s})), we have (ϵ(π)(τ ⊎ τ′) ⊎ τ ⊎ τ′)(z^{∀,w}) = τ(z^{∀,w}). Moreover, for v^{∀,s} ∈ V_{∀,s}(C(y^{∀,s})) ∪ ⊲⟨{y^{∀,s}}⟩, we have S_{π}⟨{v^{∀,s}}⟩ ⊆ S_{π}⟨{y^{∀,s}}⟩, and therefore (ϵ(π)(τ ⊎ τ′) ⊎ τ ⊎ τ′)(v^{∀,s}) = π(v^{∀,s})(_{S_{π}⟨{v^{∀,s}}⟩}|(τ ⊎ τ′)) = π(v^{∀,s})(_{S_{π}⟨{v^{∀,s}}⟩}|τ). Finally, for x^{∃} ∈ V_{∃}(C(y^{∀,s})), we have S_{e}⟨{x^{∃}}⟩ ⊆ ⊲⟨{y^{∀,s}}⟩, and therefore ϵ(e)(ϵ(π)(τ ⊎ τ′) ⊎ τ ⊎ τ′)(x^{∃}) = e(x^{∃})(_{S_{e}⟨{x^{∃}}⟩}|(ϵ(π)(τ ⊎ τ′) ⊎ τ ⊎ τ′)) = e(x^{∃})(_{S_{e}⟨\{x^{∃}\}⟩}|(_{⊲⟨\{y^{∀,s}\}⟩}|(ϵ(π)(τ ⊎ τ′)) ⊎ τ)). \underline{Q.e.d. (Claim 1)} π is well-defined by Claim 1 and obviously semantic. Thus, item 1 of Def. 5.3 is satisfied because (R ∪ S_{e} ∪ S_{π})^{+} = ⊲ is a wellfounded ordering. For showing item 2, let π ∈ V_{∀,w} → A and y^{∀,s} ∈ dom(C) and assume to the contrary that C(y^{∀,s}) is (ϵ(π)(τ) ⊎ τ, e, A)-valid, but not (_{V_{∀,s}\{y^{∀,s}}}|(ϵ(π)(τ)) ⊎ η ⊎ τ, e, A)-valid for some η ∈ {y^{∀,s}} → A. This contradicts the definition of π(y^{∀,s}) from above due to Claim 2. Q.e.d. (Lemma 5.4)

Proof of Lemma 5.6

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

First note that R′^{+} is a wellfounded ordering simply because R′ is the strong σ-update of R and σ is a strong existential R-substitution.

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

\underline{Claim 4:} For all y^{∀,s} ∈ dom(C′): For all u^{∃} ∈ V_{∃}(C′(y^{∀,s})): u^{∃}R′^{+}y^{∀,s}. \underline{Proof of Claim 4:} Let u^{∃} ∈ V_{∃}(C′(y^{∀,s})). By the definition of C′ there is some v^{∃} ∈ V_{∃}(C(y^{∀,s})) with u^{∃} (_{V_{∃}\dom(σ)}|id ∪ E_{σ}) v^{∃}. Since C is an R-choice-condition, we have v^{∃}R^{+}y^{∀,s}, i.e. u^{∃} (_{V_{∃}\dom(σ)}|id ∪ E_{σ})R^{+} y^{∀,s}. As R′ is the strong σ-update of R, we have^{17} (_{V_{∃}\dom(σ)}|id ∪ E_{σ})R^{+} ⊆ (R ∪ E_{σ})^{+} ⊆ R′^{+}. Thus u^{∃}R′^{+}y^{∀,s}. \underline{Q.e.d. (Claim 4)}

Q.e.d. (Lemma 5.6)

Proof of Lemma 5.8 As G is V_{∃}×V_{∀}-valid in A, there is some existential (A, V_{∃}×V_{∀})-valuation e such that G is (e, A)-valid. \underline{Claim 1:} e is a strong existential (A, R)-valuation. \underline{Proof of Claim 1:} As e is an existential (A, V_{∃}×V_{∀})-valuation, S_{e}∘(V_{∃}×V_{∀}) is irreflexive. This means S_{e} = ∅, i.e. (R ∪ S_{e})^{+} = R^{+}. As C is an R-choice-condition, R^{+} is a wellfounded ordering. This means that (R ∪ S_{e})^{+} is a wellfounded ordering, as was to be shown. Q.e.d. (Claim 1) By Claim 1 and Lemma 5.4, there is some π that is (e, A)-compatible with (C, R). As G is (e, A)-valid, G is also (ϵ(π)(τ), e, A)-valid for all τ ∈ V_{∀,w} → A. Then, as π is (e, A)- compatible with (C, R), G is (C, R)-strongly (e, A)-valid. Then, by Claim 1, G is (C, R)- strongly valid in A. Q.e.d. (Lemma 5.8)

Proof of Lemma 5.9

As G is (C, R)-strongly valid in A, there are some strong existential R-valuation e and some π such that π is (e, A)-compatible with (C, R) and G is strongly (π, e, A)-valid.

Set S_{e′} := (_{V_{∀,w}}|id ∪ S_{π}) ∘ S_{e}|_{V_{∃}\ran(ς)} ∪ S_{π} ∘ ς. We define e′ via: \underline{For x^{∃} ∈ V_{∃}\ran(ς):} For τ ∈ S_{e′}⟨\{x^{∃}\}⟩ → A:

e′(x^{∃})(τ) := e(x^{∃})(_{S_{e}⟨{x^{∃}}⟩}|(ϵ(π)(τ ⊎ τ′) ⊎ τ ⊎ τ′))

where τ′ ∈ (V_{∀,w}\dom(τ)) → A. Note that this right-hand side is okay because dom(τ) ⊆ V_{∀,w}; indeed S_{e′}⟨{x^{∃}}⟩ = (V_{∀,w} ∩ S_{e}⟨{x^{∃}}⟩) ∪ (S_{π} ∘ S_{e})⟨{x^{∃}}⟩ ⊆ V_{∀,w}. Furthermore, note that this right-hand side does not depend on τ′ because V_{∀,w} ∩ S_{e}⟨{x^{∃}}⟩ ⊆ S_{e′}⟨{x^{∃}}⟩ = dom(τ), and for y^{∀,s} ∈ S_{e}⟨{x^{∃}}⟩, we have S_{π}⟨{y^{∀,s}}⟩ ⊆ (S_{π} ∘ S_{e})⟨{x^{∃}}⟩ ⊆ S_{e′}⟨{x^{∃}}⟩ and therefore ϵ(π)(τ ⊎ τ′)(y^{∀,s}) = π(y^{∀,s})(_{S_{π}⟨{y^{∀,s}}⟩}|(τ ⊎ τ′)) = π(y^{∀,s})(_{S_{π}⟨{y^{∀,s}}⟩}|τ). \underline{For x^{∃} ∈ ran(ς):} For τ ∈ S_{e′}⟨\{x^{∃}\}⟩ → A:

e′(x^{∃})(τ) := π(ς^{−1}(x^{∃}))(τ).

Note that this right-hand side is okay because S_{e′}⟨{x^{∃}}⟩ = S_{π}⟨{ς^{−1}(x^{∃})}⟩ ⊆ V_{∀,w}.

\underline{Claim 1:} e′ is a strong existential (A, R′)-valuation. \underline{Proof of Claim 1:} Here we denote concatenation (product) of relations ‘∘’ simply by juxtaposition and assume it to have higher priority than any other binary operator. As π is (e, A)-compatible with (C, R), we know that (R ∪ S_{e} ∪ S_{π})^{+} is a wellfounded ordering. Thus, its subset

( (_{V_{∀,w}∪V_{∃}\ran(ς)}|id ∪ S_{π}ςς^{−1})R^{+}|_{V_{∀,w}∪V_{∃}\ran(ς)} ∪ (_{V_{∀,w}}|id ∪ S_{π})S_{e}|_{V_{∃}\ran(ς)} )^{+}

is a wellfounded ordering, too. Since the domain of this relation and dom(S_{π}) are disjoint from ran(ς), we know that

( (_{V_{∀,w}∪V_{∃}\ran(ς)}|id ∪ S_{π}ςς^{−1})R^{+}|_{V_{∀,w}∪V_{∃}\ran(ς)} ∪ (_{V_{∀,w}}|id ∪ S_{π})S_{e}|_{V_{∃}\ran(ς)} ∪ S_{π}ς )^{+}

is a wellfounded ordering, too. Since the domain of this relation and V_{∃} are disjoint from V_{∀,s}, we know that

( (_{V_{∀,w}∪V_{∃}\ran(ς)}|id ∪ S_{π}ςς^{−1})R^{+}|_{V_{∀,w}∪V_{∃}\ran(ς)} ∪ V_{∃}×V_{∀,s} ∪ (_{V_{∀,w}}|id ∪ S_{π})S_{e}|_{V_{∃}\ran(ς)} ∪ S_{π}ς )^{+}

is a wellfounded ordering, too. Since a step inside the transitive closure of the previous term that can precede ς^{−1} can only be a step with S_{π}ς (due to dom(ς^{−1}) = ran(ς) ⊆ V_{∃}),

( (_{V_{∀,w}∪V_{∃}\ran(ς)}|id ∪ ς^{−1})R^{+}|_{V_{∀,w}∪V_{∃}\ran(ς)} ∪ V_{∃}×V_{∀,s} ∪ (_{V_{∀,w}}|id ∪ S_{π})S_{e}|_{V_{∃}\ran(ς)} ∪ S_{π}ς )^{+}

is a wellfounded ordering, too. The latter relation is equal to (R′ ∪ S_{e′})^{+} which we had to show to be a wellfounded ordering. \underline{Q.e.d. (Claim 1)}

As the universes are assumed to be non-empty, there is some δ: V_{∀,s} → A by the Axiom of Choice. Define π′ by π′(y^{∀,s})(∅) := δ(y^{∀,s}).

\underline{Claim 2:} π′ is (e′, A)-compatible with (∅, R′). \underline{Proof of Claim 2:} We have S_{π′} = ∅. Thus, (R′ ∪ S_{e′} ∪ S_{π′})^{+} is equal to (R′ ∪ S_{e′})^{+}, which is a wellfounded ordering by Claim 1. \underline{Q.e.d. (Claim 2)}

\underline{Claim 3:} For τ ∈ V_{∀,w} → A and x^{∃} ∈ V_{∃}(G): ϵ(e′)(ϵ(π′)(τ) ⊎ τ)(x^{∃}) = ϵ(e)(ϵ(π)(τ) ⊎ τ)(x^{∃}). \underline{Proof of Claim 3:} We have x^{∃} ∈ V_{∃}(G) ⊆ V_{∃}\ran(ς). Thus, by the discussion of the first case of the definition of e′, we have ϵ(e′)(ϵ(π′)(τ) ⊎ τ)(x^{∃}) = e′(x^{∃})(_{S_{e′}⟨{x^{∃}}⟩}|τ) = e(x^{∃})(_{S_{e}⟨\{x^{∃}\}⟩}|(ϵ(π)(τ) ⊎ τ)) = ϵ(e)(ϵ(π)(τ) ⊎ τ)(x^{∃}). \underline{Q.e.d. (Claim 3)} \underline{Claim 4:} For τ ∈ V_{∀,w} → A and y^{∀,s} ∈ V_{∀,s}(G): ϵ(e′)(ϵ(π′)(τ) ⊎ τ)(ς(y^{∀,s})) = ϵ(π)(τ)(y^{∀,s}). \underline{Proof of Claim 4:} Since ς(y^{∀,s}) ∈ ran(ς), by the discussion of the second case of the definition of e′, we have ϵ(e′)(ϵ(π′)(τ) ⊎ τ)(ς(y^{∀,s})) = e′(ς(y^{∀,s}))(_{S_{e′}⟨{ς(y^{∀,s})}⟩}|τ) = π(ς^{−1}(ς(y^{∀,s})))(_{S_{π}⟨\{ς^{−1}(ς(y^{∀,s}))\}⟩}|τ) = π(y^{∀,s})(_{S_{π}⟨\{y^{∀,s}\}⟩}|τ) = ϵ(π)(τ)(y^{∀,s}). \underline{Q.e.d. (Claim 4)}

\underline{Claim 5:} Gς is strongly (π′, e′, A)-valid. \underline{Proof of Claim 5:} Let τ ∈ V_{∀,w} → A be arbitrary. First by the Substitution-Lemma, second by Claim 3, V_{∀,s}(G) ⊆ dom(ς), Claim 4, and third as G is strongly (π, e, A)-valid, we get: eval(A ⊎ ϵ(e′)(ϵ(π′)(τ) ⊎ τ) ⊎ ϵ(π′)(τ) ⊎ τ)(Gς) = eval(A ⊎ ϵ(e′)(ϵ(π′)(τ) ⊎ τ) ⊎ _{V_{∀,s}\dom(ς)}|(ϵ(π′)(τ)) ⊎ ς ∘ (ϵ(e′)(ϵ(π′)(τ) ⊎ τ)) ⊎ τ)(G) = eval(A ⊎ ϵ(e)(ϵ(π)(τ) ⊎ τ) ⊎ ϵ(π)(τ) ⊎ τ)(G) = TRUE \underline{Q.e.d. (Claim 5)}

\underline{Claim 6:} Gς is R′-valid. \underline{Proof of Claim 6:} First note that by Claim 1, e′ is also an existential R′-valuation. Let τ′ ∈ V_{∀} → A be arbitrary. When we set δ := _{V_{∀,s}}|τ′ and τ := _{V_{∀,w}}|τ′, we get eval(A ⊎ ϵ(e′)(τ′) ⊎ τ′)(Gς) = eval(A ⊎ ϵ(e′)(ϵ(π′)(τ) ⊎ τ) ⊎ ϵ(π′)(τ) ⊎ τ)(Gς) = TRUE, where the latter step is due to Claim 5. \underline{Q.e.d. (Claim 6)}

Now we conclude that Gς is (∅, R′)-strongly valid in A (by Claim 1, Claim 2, and Claim 5) and R′-valid (Claim 6) in A.

Q.e.d. (Lemma 5.9)

Proof of Lemma 5.11

(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′, R′). Let e be the strong existential (A, R)-valuation with ϵ(e) = ϵ(e′) and S_{e} = S_{e′} given by Lemma 3.8(1) due to R⊆R′. \underline{Claim 1:} π is (e, A)-compatible with (C, R). \underline{Proof of Claim 1:} Since π is (e′, A)-compatible with (C′, R′), ϵ(e) = ϵ(e′), and S_{e} = S_{e′}, π is (e, A)-compatible with (C′, R′). Since C⊆C′, π is (e, A)-compatible with (C, R′). Since R⊆R′, π is (e, A)-compatible with (C, R). \underline{Q.e.d. (Claim 1)}

\underline{(5a):} As G_{0} is (C′, R′)-strongly valid in A, there is some a strong existential (A, R′)-valu-ation e′ and some π such that π is (e′, A)-compatible with (C′, R′) and G_{0} is strongly (π, e′, A)-valid. Let e be given as in (5) above. As ϵ(e) = ϵ(e′), G_{0} is strongly (π, e, A)- valid. Thus, by Claim 1, G_{0} is (C, R)-strongly (e, A)-valid. As e is a strong existential (A, R)-valuation, G_{0} is (C, R)-strongly valid in A.

\underline{(5b):} Let e′, π, and e be given as in (5) above and suppose that G_{1} is strongly (π, e′, A)- valid. As ϵ(e) = ϵ(e′), G_{1} is strongly (π, e, A)-valid, too. Thus, by Claim 1 and since e is a strong existential (A, R)-valuation and G_{0} (C, R)-strongly reduces to G_{1}, also G_{0} is strongly (π, e, A)-valid. As ϵ(e) = ϵ(e′), this also means that G_{0} is strongly (π, e′, A)-valid as was to be shown.

\underline{(6):} Let e′ be a strong existential (A, R′)-valuation and π be (e′, A)-compatible with (C′, R′). Let e be the strong existential (A, R)-valuation given by Lemma 3.8(2) due to σ being a strong existential R-substitution and R′ the strong σ-update of R. Then, for all δ ∈ V_{∀} → A,

ϵ(e)(δ) = (_{V_{∃}\dom(σ)}|id ∪ σ) ∘ eval(A ⊎ ϵ(e′)(δ) ⊎ δ)

and S_{e} = S_{e′} ∘ (_{V_{∃}\dom(σ)}|id ∪ E_{σ}) ∪ U_{σ} \underline{Claim 2:} For any set of sequents G′ and any δ ∈ V_{∀} → A:

(δ, e, A)-validity of G′ is logically equivalent to (δ, e′, A)-validity of G′σ. \underline{Proof of Claim 2:} For y ∈ V_{∀} we have: δ(y) = eval(A ⊎ ϵ(e′)(δ) ⊎ δ)(y), i.e. by the above:

ϵ(e)(δ) ⊎ δ = (_{V_{free}\dom(σ)}|id ∪ σ) ∘ eval(A ⊎ ϵ(e′)(δ) ⊎ δ).

Thus, for any formula B, we have

eval(A ⊎ ϵ(e)(δ) ⊎ δ)(B)  =
eval(A ⊎ (_{V_{free}\dom(σ)}|id ∪ σ) ∘ eval(A ⊎ ϵ(e′)(δ) ⊎ δ))(B) =
eval(A ⊎ ϵ(e′)(δ) ⊎ δ)(Bσ),

the latter step being due to the Substitution-Lemma. \underline{Q.e.d. (Claim 2)} \underline{Claim 3:} (R ∪ S_{e} ∪ S_{π})^{+} is a wellfounded ordering. \underline{Proof of Claim 3:} As π is (e′, A)-compatible with (C′, R′), we know that (R′ ∪ S_{e′} ∪ S_{π})^{+} is a wellfounded ordering. As R′ is the strong σ-update of R, we have^{18} R′ = R ∪ E_{σ} ∪ U_{σ} and (R ∪ E_{σ} ∪ U_{σ} ∪ S_{e′} ∪ S_{π})^{+} is a wellfounded ordering, just like its subset (R ∪ S_{e′} ∘ (_{V_{∃}\dom(σ)}|id ∪ E_{σ}) ∪ U_{σ} ∪ S_{π})^{+}, which is equal to (R ∪ S_{e} ∪ S_{π})^{+}. Q.e.d. (Claim 3) \underline{Claim 4:} Let τ ∈ V_{∀,w} → A, y^{∀,s} ∈ dom(C), and suppose that C(y^{∀,s}) is (ϵ(π)(τ) ⊎ τ, e, A)- valid. Now: C(y^{∀,s}) is (_{V_{∀,s}\{y^{∀,s}}}|(ϵ(π)(τ)) ⊎ η ⊎ τ, e, A)-valid for all η ∈ {y^{∀,s}} → A. \underline{Proof of Claim 4:} As (C′, R′) is the extended σ-update of (C, R), we have C′(y^{∀,s}) = (C(y^{∀,s}))σ. Thus, by Claim 2, C′(y^{∀,s}) is (ϵ(π)(τ) ⊎ τ, e′, A)-valid. By Lemma 5.6, C′ is an R′-choice-condition. Therefore, we know that C′(y^{∀,s}) is (_{V_{∀,s}\{y^{∀,s}}}|(ϵ(π)(τ)) ⊎ η ⊎ τ, e′, A)- valid for all η ∈ {y^{∀,s}} → A. By Claim 2, C(y^{∀,s}) is (_{V_{∀,s}\{y^{∀,s}}}|(ϵ(π)(τ)) ⊎ η ⊎ τ, e, A)-valid for all η ∈ \{y^{∀,s}\} → A. \underline{Q.e.d. (Claim 4)} \underline{Claim 5:} π is (e, A)-compatible with (C, R). \underline{Proof of Claim 5:} Since π is (e′, A)-compatible with (C′, R′), this is a consequence of Claim 3 and Claim 4. \underline{Q.e.d. (Claim 5)} \underline{Claim 6:} For any set of sequents G′: strong (π, e, A)-validity of G′ is logically equivalent to strong (π, e′, A)-validity of G′σ. \underline{Proof of Claim 6:} This is a trivial consequence of Claim 2. \underline{Q.e.d. (Claim 6)}

\underline{(6a):} As G_{0}σ is (C′, R′)-strongly valid in A, there is some a strong existential (A, R′)-valu-ation e′ and some π such that π is (e′, A)-compatible with (C′, R′) and G_{0}σ is strongly (π, e′, A)-valid. Let e be given as in (6) above. By Claim 6, G_{0} is strongly (π, e, A)-valid. By Claim 5 and as e is a strong existential (A, R)-valuation, G_{0} is (C, R)-strongly valid in A.

\underline{(6b):} Let e′ be a strong existential (A, R′)-valuation, π be (e′, A)-compatible with (C′, R′), and suppose that G_{1}σ is strongly (π, e′, A)-valid. Let e the strong existential (A, R)-valu-ation of (6) above. Then, by Claim 5, π is (e, A)-compatible with (C, R), and, by Claim 6, G_{1} is strongly (π, e, A)-valid. By assumption, G_{0} strongly (C, R)-reduces to G_{1}. Thus, G_{0} is strongly (π, e, A)-valid, too. By Claim 6, this means that G_{0}σ is strongly (π, e′, A)-valid as was to be shown.

Q.e.d. (Lemma 5.11)

Proof of Theor. 5.14 Since AX is assumed to be V_{∃}×V_{∀}-valid (cf. Def. 4.6), AX is (C, R)-strongly valid by Lemma 5.8. Set T := { t′ | (i′, (Γ′, t′)) ∈ F ∧ i′L^{∗}i }. Since all trees in T are closed, we have Goals(T) ⊆ AX . Thus, Goals(T) is (C, R)-strongly valid. Since (i, (Γ, t)) ∈ F and (F, C, R, L) satisfies the strong soundness invariant condition, {Γ } strongly (C, R)-reduces to Goals(T). All in all, by Lemma 5.11(1), Γ is (C, R)-strongly valid. Finally, by Lemma 5.9, Γ ς is (∅, R′)-strongly valid and (weakly) R′-valid. Q.e.d. (Theor. 5.14)

Proof of Theor. 5.16

(∅, ∅, ∅, ∅) trivially satisfies the strong soundness invariant condition.

For the iteration steps, we let (i′′, (Γ′′, t′′)) ∈ F′ be arbitrary and set

T (i) := { t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F′ ∧ i′′′L′^{∗}i }.

Assuming the strong soundness invariant condition for the strong proof forest (F, C, R, L), we have to show that C′ is an R′-choice-condition and that

{Γ′′} strongly (C′, R′)-reduces to Goals(T (i′′)).

Hypothesizing: Note that F′ is a partial function on IN_{+} just like F because of i ∈ IN_{+} \ dom(F). Note that R is a variable-condition and that R^{+} is a wellfounded ordering because C is an Rchoice-condition (because (F, C, R, L) is assumed to be a strong proof forest). Moreover, due to C′ = C, R′ = R∪R′′, and ran(R′′)∩dom(R′) = ∅ being assumed for the variablecondition R′′ in the first alternative case of the Hypothesizing rule, we know that R′^{+} is a wellfounded ordering and (C′, R′) is an extension of (C, R). Thus, in any case, (C′, R′) is an extension of (C, R). \underline{(i′′, (Γ′′, t′′)) ∈ F:}

{Γ′′} strongly (C, R)-reduces to Goals({ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ }) by assumption, and then, due to Lemma 5.11(5b),

{Γ′′} strongly (C′, R′)-reduces to Goals({ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ }). Thus, by Lemma 5.11(2,3), we only have to show { t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ } ⊆ T (i′′). But this follows from L = L′ and F ⊆F′. \underline{(i′′, (Γ′′, t′′)) = (i, (Γ, t)):} Then \{Γ′′\} = \{Γ \} = Goals(\{t\}) = Goals(\{t′′\}) ⊆ Goals(T (i′′)). Thus, by Lemma 5.11(2), {Γ′′} strongly (C′, R′)-reduces to Goals(T (i′′)).

\underline{\underline{Expansion:}} \underline{Claim 1:} For n ∈ N, (Π, t′′′′) = F (n): \{Π\} strongly (C′, R′)-reduces to Goals(T (i)). Proof of Claim 1:

{Π} strongly (C, R)-reduces to Goals({ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}n }) by assumption. Thus, due to (C′, R′) being an extension of (C, R) and Lemma 5.11(5b),

{Π} strongly (C′, R′)-reduces to Goals({ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}n }).

Since L^{∗} ∩ ({i}×N) = ∅, _{IN_{+}\{i}}|F′ =_{IN_{+}\{i}}|F , and L′ = L ∪ N×{i}, we have

\begin{aligned}\{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}n \} & = \\ \{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}n ∧ i′′′ ≠ i \} & ⊆ \\ \{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F′ ∧ i′′′L^{∗}n \} & ⊆ \\ \{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F′ ∧ i′′′L′^{∗}i \} & = T (i). \end{aligned}

Thus, by Lemma 5.11(2,3), \{Π\} strongly (C′, R′)-reduces to Goals(T (i)). \underline{Q.e.d. (Claim 1)} \underline{Claim 2:} Goals(\{t\}) strongly (C′, R′)-reduces to Goals(T (i)). \underline{Proof of Claim 2:} As Goals(\{t\})\\{Δ\} ⊆ Goals(\{t′\}) ⊆ Goals(\{t′\}) ∪ dom(⟨N⟩F), by Lemma 5.11(2),

Goals({t})\{Δ} strongly (C′, R′)-reduces to Goals({t′}) ∪ dom(⟨N⟩F). Thus, since by assumption

{Δ} strongly (C′, R′)-reduces to a subset of Goals({t′}) ∪ dom(⟨N⟩F), by Lemma 5.11(4),

Goals({t}) strongly (C′, R′)-reduces to Goals({t′}) ∪ dom(⟨N⟩F).

Moreover, since {t′} ⊆ T (i), by Lemma 5.11(2), Goals({t′}) strongly (C′, R′)-reduces to Goals(T (i)). Thus, by Claim 1 and Lemma 5.11(4),

Goals({t′}) ∪ dom(⟨N⟩F) strongly (C′, R′)-reduces to Goals(T (i)).

Thus, by Lemma 5.11(3), Goals({t}) strongly (C′, R′)-reduces to Goals(T (i)). Q.e.d. (Claim 2)

By assumption

{Γ′′} strongly (R, C)-reduces to Goals({ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ }). Thus, due to (C′, R′) being an extension of (C, R) and Lemma 5.11(5b),

{Γ′′} strongly (C′, R′)-reduces to Goals({ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ }).

\underline{(i, i′′) ∉ L^{∗}:} Since _{IN_{+}\\{i\}}|F′ =_{IN_{+}\\{i\}}|F , L⊆L′ we have

\begin{aligned}\{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ \} & = \\ \{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ ∧ i′′′ ≠ i \} & ⊆ \\ \{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F′ ∧ i′′′L^{∗}i′′ \} & ⊆ \\ \{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F′ ∧ i′′′L′^{∗}i′′ \} & = T (i′′). \end{aligned}

Thus, by Lemma 5.11(2),

Goals({ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ }) strongly (C′, R′)-reduces to Goals(T (i′′)). Thus, by Lemma 5.11(3), {Γ′′} strongly (C′, R′)-reduces to Goals(T (i′′)).

\underline{(i, i′′) ∈ L^{∗}:} Since _{IN_{+}\\{i\}}|F′ =_{IN_{+}\\{i\}}|F , L⊆L′ we have

\begin{aligned}\{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ \} & = \\ \{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ ∧ i′′′ ≠ i \} ∪ \{t\} & ⊆ \\ \{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F′ ∧ i′′′L^{∗}i′′ \} ∪ \{t\} & ⊆ \\ \{ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F′ ∧ i′′′L′^{∗}i′′ \} ∪ \{t\} & = T (i′′) ∪ \{t\}. \end{aligned}

Thus, by Lemma 5.11(2,3),

{Γ′′} strongly (C′, R′)-reduces to Goals(T (i′′)) ∪ Goals({t}).

By Lemma 5.11(2), Goals(T (i′′)) strongly (C′, R′)-reduces to Goals(T (i′′)). Thus, by Claim 2 and Lemma 5.11(4), Goals(T (i′′)) ∪ Goals({t}) strongly (C′, R′)-reduces to Goals(T (i′′)) ∪ Goals(T (i)) = Goals(T (i′′)). The latter equality holds because we have T (i) ⊆ T (i′′) here. Finally, by Lemma 5.11(3),

{Γ′′} strongly (C′, R′)-reduces to Goals(T (i′′)).

\underline{\underline{Instantiation:}} By Lemma 5.6, C′ is an R′-choice-condition. Set (Γ, t) := F (i′′). Then Γ′′ = Γ σ. By assumption,

{Γ } strongly (R, C)-reduces to Goals({ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ }). By Lemma 5.11(6b), {Γ′′} strongly (C′, R′)-reduces to Goals({ t′′′σ | (i′′′, (Γ′′′, t′′′)) ∈ F ∧ i′′′L^{∗}i′′ }) = Goals({ t′′′ | (i′′′, (Γ′′′, t′′′)) ∈ F′ ∧ i′′′L^{∗}i′′ }) = Goals(T (i′′)).

Q.e.d. (Theor. 5.16)

Proof of Theor. 5.19

The empty proof forest trivially satisfies the strong safeness invariant condition.

\underline{\underline{Hypothesizing:}} When we assume the old trees from F to satisfy the strong safeness invariant condition for (C, R), then they also satisfy it for (C′, R′) by Lemma 5.11(5b). The new tree (i, (Γ, t)) satisfies the strong safeness invariant condition because Goals({t}) = {Γ } and {Γ } (C′, R′)-strongly reduces to {Γ } by Lemma 5.11(2).

\underline{\underline{Expansion:}} When we assume the non-expanded trees to satisfy the strong safeness invariant condition for (C, R), then they also satisfy it for (C′, R′) by Lemma 5.11(5b). For the new tree (i, (Γ, t′)) we have to show that Goals({t′}) (C′, R′)-strongly reduces to {Γ }. \underline{Claim 1:} Goals(\{t′\}) (C′, R′)-strongly reduces to Goals(\{t\}). \underline{Proof of Claim 1:} In case of the tableau calculus,

{ ΛΔ | Λ ∈ G } (C′, R′)-strongly reduces to {Δ}

because strong (π, e, A)-validity of Δ implies strong (π, e, A)-validity of ΛΔ. Moreover,

Goals({t′}) \ { ΛΔ | Λ ∈ G } (C′, R′)-strongly reduces to Goals({t})

by Lemma 5.11(2) due to Goals({t′}) \ { ΛΔ | Λ ∈ G } ⊆ Goals({t}). Thus, the claim follows by Lemma 5.11(4) due to Δ ∈ Goals({t}). In case of the sequent calculus, we have the additional requirement of safeness of the Expansion step, i.e.

G (C′, R′)-strongly reduces to {Δ}.

Moreover,

Goals({t′}) \ G (C′, R′)-strongly reduces to Goals({t})

by Lemma 5.11(2) due to Goals({t′}) \ G ⊆ Goals({t}). Thus, the claim follows by Lemma 5.11(4) due to Δ ∈ Goals(\{t\}). \underline{Q.e.d. (Claim 1)} When we assume the old tree (i, (Γ, t)) to satisfy the safeness invariant condition for R, then Goals({t}) (C′, R′)-strongly reduces to {Γ } by Lemma 5.11(5b). By Lemma 5.11(3), together with Claim 1 this implies that Goals({t′}) (C′, R′)-strongly reduces to {Γ }, as was to be shown.

\underline{\underline{Instantiation:}} By Lemma 5.11(6b).

Q.e.d. (Theor. 5.19)

Proof of Theor. 5.20

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{\underline{α-rule:}} We have to show that \{Γ (A∨B) Π\} strongly (C, R)-reduces to \{A B Γ Π\} in A and vice versa. This is trivial, however, because strong (π, e, A)-validity of the two sets is logically equivalent for each strong existential (A, R)-valuation e and each π that is (e, A)-compatible with (C, R).

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

\underline{\underline{γ-rule:}} We have to show that

{Γ ∃x: A Π} strongly (C, R)-reduces to {A{x↦x^{∃}} Γ ∃x: A Π}

in A and vice versa. This is the case, however, because strong (π, e, A)-validity of the two sets is logically equivalent for each strong existential (A, R)-valuation e and each π that is (e, A)-compatible with (C, R). The implication from left to right is given because the former sequent is a sub-sequent of the latter. For the other direction, note that, for any τ ∈ V_{∀,w} → A, when we set δ := ϵ(π)(τ) ⊎ τ, it is clear that (δ, 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 rule 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 strongly (π, e, A)-valid for some strong existential (A, R)-valuation e and some π that is (e, A)-compatible with (C, R). We have to show that the former sequent is strongly (π, e, A)-valid. If this is not the case, there must be some τ ∈ V_{∀,w} → A such that the former sequent is not (δ, e, A)-valid for δ := ϵ(π)(τ) ⊎ τ. Since the latter sequent must be (δ, e, A)-valid, we know that 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.5), 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, which is a contradiction.

\underline{\underline{δ-rule:}} Note that in this proof for soundness, we only make use of the weaker conditions on the occurrence of x^{∀,w} given by Note 2.

\underline{Claim 1:} (C′, R′) is an extension of (C, R). \underline{Proof of Claim 1:} Since (F, C, R, L) is a strong proof forest, C is an R-choice-condition. Moreover, C⊆C′ and R⊆R′ are trivial. Thus, we only have to show that C′ is an R′-choice-condition. As C′ = C, we only have to show that R′^{+} is a wellfounded ordering. As ran(R′′) = {x^{∀,w}} and {x^{∀,w}}∩dom(R) = ∅ is required, we have R′′∘R = ∅. As ran(R′′)∩ dom(R′′) ⊆ {x^{∀,w}} ∩ V(A, Γ Π) = ∅ is required, we have R′′∘R′′ = ∅. Therefore, as R^{+} is a wellfounded ordering, R′^{+} is a wellfounded ordering, too. \underline{Q.e.d. (Claim 1)}

Now, we have to show that

{Γ ∀x:A Π} strongly (C′, R′)-reduces to {A{x↦x^{∀,w}} Γ Π}

in A and vice versa. Let e and π be arbitrary such that e is a strong existential (A, R′)- valuation and π is (e, A)-compatible with (C′, R′).

For the one direction, assume that the latter sequent is strongly (π, e, A)-valid. For arbitrary τ ∈ V_{∀,w} → 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_{∀,w} → A with _{V_{∀,w}\{x^{∀,w}}}|τ′ = _{V_{∀,w}\{x^{∀,w}}}|τ, simply because x^{∀,w} does not occur in Γ Π. \underline{Claim 2:} Γ Π is invalid in A ⊎ ϵ(e)(ϵ(π)(τ′) ⊎ τ′) ⊎ ϵ(π)(τ′) ⊎ τ′ for all τ′ ∈ V_{∀,w} → A with V_{∀,w}\{x^{∀,w}}|τ′ = _{V_{∀,w}\{x^{∀,w}}}|τ. \underline{Proof of Claim 2:} Otherwise there must be some u ∈ V_{∀,s}(Γ Π)∪V_{∃}(Γ Π) with x^{∀,w} S_{π} ∘ S_{e} u (the first occurrence of τ′ makes a difference) or x^{∀,w} S_{e} u (the second occurrence of τ′ makes a difference) or x^{∀,w} S_{π} u when the third occurrence of τ′ makes a difference. Since u R′′ x^{∀,w}, we know that (R′ ∪ S_{e} ∪ S_{π})^{+} is not a wellfounded ordering, which contradicts π being (e, A)-compatible with (C′, R′). \underline{Q.e.d. (Claim 2)} Since the latter sequent is assumed to be strongly (π, e, A)-valid, Claim 2 means that A{x↦x^{∀,w}} is valid in A ⊎ ϵ(e)(ϵ(π)(τ′) ⊎ τ′) ⊎ ϵ(π)(τ′) ⊎ τ′ for all τ′ ∈ V_{∀,w} → A with V_{∀,w}\{x^{∀,w}}|τ′ = _{V_{∀,w}\{x^{∀,w}}}|τ. \underline{Claim 3:} A\{x↦x^{∀,w}\} is valid in A ⊎ ϵ(e)(ϵ(π)(τ) ⊎ τ) ⊎ ϵ(π)(τ) ⊎ τ′ for all τ′ ∈ V_{∀,w} → A with _{V_{∀,w}\{x^{∀,w}}}|τ′ = _{V_{∀,w}\{x^{∀,w}}}|τ. \underline{Proof of Claim 3:} Otherwise there must be some u ∈ V_{∀,s}(A\{x↦x^{∀,w}\})∪V_{∃}(A\{x↦x^{∀,w}\}) with x^{∀,w} S_{π} ∘ S_{e} u (the first occurrence of τ′ makes a difference) or x^{∀,w} S_{e} u (the second occurrence of τ′ makes a difference) or x^{∀,w} S_{π} u when the third occurrence of τ′ makes a difference. Since u R′′ x^{∀,w}, we know that (R′ ∪ S_{e} ∪ S_{π})^{+} is not a wellfounded ordering, which contradicts π being (e, A)-compatible with (C′, R′). \underline{Q.e.d. (Claim 3)} 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.5), Claim 3 means that ∀x:(A{x↦x^{∀,w}}{x^{∀,w}↦x}) is valid in A⊎ϵ(e)(ϵ(π)(τ) ⊎ τ)⊎ϵ(π)(τ)⊎τ, i.e. (ϵ(π)(τ) ⊎ τ, e, A)-valid. Since x^{∀,w} 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.

For the vice versa direction, assume that the former sequent is strongly (π, e, A)-valid. For arbitrary τ ∈ V_{∀,w} → A we have to show that the latter sequent is (δ, e, A)-valid for δ := ϵ(π)(τ)⊎τ. If some formula in Γ Π is (δ, e, A)-valid, then the former sequent is (δ, e, A)- valid, too. Otherwise, ∀x:A is (δ, e, A)-valid. Then, by the standard semantic definition of ∀, A{x↦x^{∀,w}} is (δ, e, A)-valid, too, as was to be shown.

Liberalized δ-rule: Note that in this proof for soundness, we only make use of the weaker conditions on the occurrence of x^{∀,s} given by Note 3.

\underline{Claim 4:} (C′, R′) is an extension of (C, R). \underline{Proof of Claim 4:} Since (F, C, R, L) is a strong proof forest, C is an R-choice-condition. Moreover, C⊆C′ and R⊆R′ are trivial. Thus, we only have to show that C′ is an R′-choice-condition. As x^{∀,s} ∈ V_{∀,s}\dom(C) is required, C′ is also a partial function on V_{∀,s}. As ran(R′′) = {x^{∀,s}} and {x^{∀,s}}∩dom(R) = ∅ is required, we have R′′∘R = ∅. As ran(R′′) ∩ dom(R′′) = {x^{∀,s}} ∩ V_{free}(A) = {x^{∀,s}} ∩ V(A) = ∅ is required, we have R′′∘R′′ = ∅. Therefore, as R^{+} is a wellfounded ordering, R′^{+} is a wellfounded ordering, too.

Moreover, for y^{∀,s} ∈ dom(C′), we either have y^{∀,s} ∈ dom(C) and then (V_{free}(C′(y^{∀,s}))\{y^{∀,s}})×{y^{∀,s}} = (V_{free}(C(y^{∀,s}))\{y^{∀,s}})×{y^{∀,s}} ⊆ R^{+} ⊆ R′^{+}, or y^{∀,s} = x^{∀,s} and then (V_{free}(C′(y^{∀,s}))\{y^{∀,s}})×{y^{∀,s}} = (V_{free}(A{x↦x^{∀,s}})\{x^{∀,s}})×{x^{∀,s}} ⊆ V_{free}(A)×{x^{∀,s}} = R′′ ⊆ R′^{+}. \underline{Q.e.d. (Claim 4)}

Now, we have to show that

{Γ ∀x:A Π} strongly (C′, R′)-reduces to {A{x↦x^{∀,s}} Γ Π}

in A and vice versa. Let e and π be arbitrary such that e is a strong existential (A, R′)- valuation and π is (e, A)-compatible with (C′, R′). Let τ ∈ V_{∀,w} → A be arbitrary and set δ := ϵ(π)(τ) ⊎ τ.

For the one direction, assume that the latter sequent is strongly (π, e, A)-valid. 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^{∀,s}} is (δ, e, A)-valid. Since π is (e, A)-compatible with (C′, R′), by item 2 of Def. 5.3, we know that A{x↦x^{∀,s}} is (δ′, e, A)-valid for all δ′ ∈ V_{∀} → A with _{V_{∀}\{x^{∀,s}}}|δ′ = _{V_{∀}\{x^{∀,s}}}|δ. This means that A{x↦x^{∀,s}} is valid in A⊎ϵ(e)(δ′)⊎δ′ for all δ′ ∈ V_{∀} → A with _{V_{∀}\{x^{∀,s}}}|δ′ = _{V_{∀}\{x^{∀,s}}}|δ. \underline{Claim 5:} A\{x↦x^{∀,s}\} is valid in A⊎ϵ(e)(δ)⊎δ′ for all δ′ ∈ V_{∀} → A with_{V_{∀}\\{x^{∀,s}\}}|δ′ =_{V_{∀}\\{x^{∀,s}\}}|δ. \underline{Proof of Claim 5:} Otherwise we have x^{∀,s}S_{e}u^{∃} for some u^{∃} ∈ V_{∃}(A\{x↦x^{∀,s}\}). But then u^{∃} ∈ V_{free}(A) and then u^{∃}R′′x^{∀,s}. This means that (R′ ∪ S_{e})^{+} is not a wellfounded ordering, which contradicts e being a strong existential (A, R′)-valuation. \underline{Q.e.d. (Claim 5)} 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.5), Claim 5 means that ∀x:(A{x↦x^{∀,s}}{x^{∀,s}↦x}) is valid in A ⊎ ϵ(e)(δ) ⊎ δ. Since x^{∀,s} 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.

For the vice versa direction, assume that the former sequent is strongly (π, e, A)- valid. We have to show that the latter sequent is (δ, e, A)-valid. If some formula in Γ Π is (δ, e, A)-valid, then the former sequent is (δ, e, A)-valid, too. Otherwise, ∀x:A is (δ, e, A)- valid. Then, by the standard semantic definition of ∀, A{x↦x^{∀,s}} is (δ, e, A)-valid, too, as was to be shown.

\underline{\underline{Rewrite-rule:}} We have to show that

{Γ A[s] Π B Λ} strongly (C, R)-reduces to {A[t] Γ Π B Λ}

in A and vice versa. This is the case, however, because strong (π, e, A)-validity of the two sets is logically equivalent for each strong existential (A, R)-valuation e and each π that is (e, A)-compatible with (C, R). For arbitrary τ ∈ V_{∀,w} → A it is sufficient to show that (δ, e, A)-validity of the two sequents is equivalent for δ := ϵ(π)(τ) ⊎ τ. If eval(A ⊎ ϵ(e)(δ) ⊎ δ)(s) ≠ eval(A ⊎ ϵ(e)(δ) ⊎ δ)(t), then both are (δ, e, A)-valid because B is. Otherwise, we set a := eval(A ⊎ ϵ(e)(δ) ⊎ δ)(s), choose some z^{∀} ∈ V_{∀}\V(A[s]), and define δ′ ∈ V_{∀} → A by _{V_{∀}\{z^{∀}}}|δ′ =_{V_{∀}\{z^{∀}}}|δ and δ′(z^{∀}) = a. Then a = eval(A ⊎ ϵ(e)(δ) ⊎ δ)(t). Moreover, by the Substitution-Lemma:

eval(A ⊎ ϵ(e)(δ) ⊎ δ)(A[s])  =
eval(A ⊎ ϵ(e)(δ) ⊎ δ)(A[z^{∀}]{z^{∀}↦s}) =
eval(A ⊎ ϵ(e)(δ) ⊎ δ′)(A[z^{∀}])  =
eval(A ⊎ ϵ(e)(δ) ⊎ δ)(A[z^{∀}]{z^{∀}↦t}) =
eval(A ⊎ ϵ(e)(δ) ⊎ δ)(A[t]).

Note that the usual problems with variables getting captured by quantifiers cannot occur in our context, because the formula (s≠t) cannot contain any variables from V_{bound} because it cannot contain any quantifiers and the unbound occurrence of variables from V_{bound} in formulas is not permitted, cf. Section 1.5.

Q.e.d. (Theor. 5.20)

Proof of Theor. 5.22 \underline{Claim 1:} C′ is an R′-choice-condition. \underline{Proof of Claim 1:} For the one alternative we have C′ = C and R′ is a variable-condition such that R⊆R′ and R′^{+} is a wellfounded ordering. Since (F, C, R, L) is a strong proof forest, C is an R-choice-condition. Thus, for y^{∀,s} ∈ dom(C′), we have y^{∀,s} ∈ dom(C) and then (V_{free}(C′(y^{∀,s}))\{y^{∀,s}}) × {y^{∀,s}} = (V_{free}(C(y^{∀,s}))\{y^{∀,s}}) × {y^{∀,s}} ⊆ R^{+} ⊆ R′^{+}. For the other alternative the claim is trivially satisfied. \underline{Q.e.d. (Claim 1)} According to the definition of an Expansion step in the tableau calculus of Def. 5.15 we still have to show that {Δ} strongly (C′, R′)-reduces to { AΔ | A ∈ G } ∪ {Π}. Thus, for A ∈ K, e a strong existential (A, R′)-valuation, and π (e, A)-compatible with (C′, R′), it suffices to refute the assumption that { AΔ | A ∈ G }∪{Π} is strongly (π, e, A)-valid, but Δ is not. Then there is some τ ∈ V_{∀,w} → A such that Δ is not (ϵ(π)(τ)⊎τ, e, A)-valid. Since all AΔ with A ∈ G must be (ϵ(π)(τ) ⊎ τ, e, A)-valid, we know that G is (ϵ(π)(τ) ⊎ τ, e, A)- valid. By the definition of G, this means that Πϱ is not (ϵ(π)(τ) ⊎ τ, e, A)-valid.

Define τ′ ∈ V_{∀,w} → A by τ′(y^{∀,w}) := \{ \begin{matrix}ϵ(e)(ϵ(π)(τ) ⊎ τ)(ϱ(y^{∀,w})) & for y^{∀,w} ∈ Y \\ τ(y^{∀,w}) & for y^{∀,w} ∈ V_{∀,w}\Y \end{matrix} \} .

\underline{Claim 2:} For v^{∀,s} ∈ V_{∀,s}(Π) we have ϵ(π)(τ)(v^{∀,s}) = ϵ(π)(τ′)(v^{∀,s}). \underline{Proof of Claim 2:} Otherwise there must be some y^{∀,w} ∈ Y with y^{∀,w} S_{π} v^{∀,s}. Since v^{∀,s} ∈ V_{∀,s}(Π) we have v^{∀,s} R′ y^{∀,w} by definition of Y. But then (R′ ∪ S_{e} ∪ S_{π})^{+} is not a wellfounded ordering, which contradicts π being (e, A)-compatible with (C′, R′). Q.e.d. (Claim 2) \underline{Claim 3:} For x^{∃} ∈ V_{∃}(Π) we have ϵ(e)(ϵ(π)(τ) ⊎ τ)(x^{∃}) = ϵ(e)(ϵ(π)(τ′) ⊎ τ′)(x^{∃}). \underline{Proof of Claim 3:} Otherwise there must be some y^{∀,w} ∈ Y with y^{∀,w} S_{π} ∘ S_{e} x^{∃} (i.e. the first occurrence of τ′ makes a difference) or y^{∀,w} S_{e} x^{∃} when the second occurrence of τ′ makes a difference. Since x^{∃} ∈ V_{∃}(Π) we have x^{∃} R′ y^{∀,w} by definition of Y. But then (R′ ∪ S_{e} ∪ S_{π})^{+} is not a wellfounded ordering, which contradicts π being (e, A)-compatible with (C′, R′). \underline{Q.e.d. (Claim 3)} Now we have eval(A ⊎ ϵ(e)(ϵ(π)(τ′) ⊎ τ′) ⊎ ϵ(π)(τ′) ⊎ τ′)(Π) = eval(A ⊎ ϵ(e)(ϵ(π)(τ′) ⊎ τ′) ⊎ ϵ(π)(τ) ⊎ τ′)(Π) = eval(A ⊎ ϵ(e)(ϵ(π)(τ) ⊎ τ) ⊎ ϵ(π)(τ) ⊎ τ′)(Π) = eval(A ⊎ ϵ(e)(ϵ(π)(τ) ⊎ τ) ⊎ ϵ(π)(τ) ⊎ τ)(Πϱ) = FALSE

for the following reasons: First: By Claim 2. Second: By Claim 3. Third: By the Substitution-Lemma. Fourth: As Πϱ is not (ϵ(π)(τ) ⊎ τ, e, A)-valid. Thus, Π is not (ϵ(π)(τ′) ⊎ τ′, e, A)-valid, i.e. not strongly (π, e, A)-valid, which contradicts our assumption from above. Q.e.d. (Theor. 5.22)

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.

Herbert B. Enderton (1973). A Mathematical Introduction to Logic. Academic Press, 2^{nd} printing.

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..

David Hilbert, Paul Bernays (1968/70). Grundlagen der Mathematik. 2^{nd} ed., Springer.

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 (1998a). Full First-Order Sequent and Tableau Calculi With Preservation of Solutions and the Liberalized δ-Rule but Without Skolemization. Report 698/1998, FB Informatik, Univ. Dortmund. Short version: Wirth (1998b).

Claus-Peter Wirth (1998b). 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’98), pp. 244-255, Tech. Univ. Vienna, 1998. Also in: Gernot Salzer, Ricardo Caferra (eds.). Automated Deduction in Classical and Non-Classical Logics. LNAI 1761, pp. 283-298, Springer, 2000. Long version: Wirth (1998a).

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.

Note 1: Note that x^{∃} ∉ V_{∃}(F, C, R, L) is not required for soundness (cf. the proofs of Theor. 4.14 and Theor. 5.20), but only in order not to lose possible proofs.

Note 2: Note that for soundness of the δ-rule x^{∀,w} ∉ V(A, Γ Π) ∪ dom(R) is sufficient, cf. the proofs of Theor. 4.14 and Theor. 5.20. Nevertheless, we require x^{∀,w} ∉ V(F, C, R, L) in order not to lose possible proofs.

Note 3: Note that for soundness of the liberalized δ-rule x^{∀,s} ∉ V(A) ∪ dom(C∪R) is sufficient, cf. the proof of Theor. 5.20. Nevertheless, we require x^{∀,s} ∉ V(F, C, R, L) in order not to lose possible proofs.

Note 4: For 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.

Note 5: The 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.

Note 6: We 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).

Note 7: Note 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.

Note 8: If you nevertheless want to have re-use of free existential variables and name switches, you have use the following alternative notions instead.

Definition Note 8.1 (Alternative Variable-Condition) (Cf. Def. 1.1) A variable-condition is a subset of V_{free} × V_{∀}.

Definition Note 8.2 (Alternative [Strong] Existential R-Substitution) (Cf. Def. 3.2) 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 ((_{V_{free}\dom(σ)}|id ∪ E_{σ} ∪ U_{σ}) ∘ R)^{+} is a wellfounded ordering.

Definition Note 8.3 (Alternative [Strong] σ-Update) (Cf. Def. 3.3) Let R be a variable-condition and σ be an [strong] existential R-substitution. The σ-update of R is (_{V_{free}\dom(σ)}|id ∪ E_{σ}) ∘ R. The strong σ-update of R is (_{V_{free}\dom(σ)}|id ∪ E_{σ} ∪ U_{σ}) ∘ R.

In an implementation, substituted free existential variables should get new nodes while their old nodes lose their labels. E.g., (where we have boxed the old occurrences of the re-used free existential variables x^{∃} and u^{∃}) for

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

and the strong R-substitution (in the alternative sense!)

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

we would update

\begin{aligned}u^{∃} & \overline{_{_{R} >}} & v^{∀,s} & < _{R} & w^{∃} \\ y^{∀,s} & < _{R} & x^{∃} \end{aligned}

first to

\begin{aligned}x^{∃} & \overline{_{_{E_{σ}} >}} & u^{∃} & \overline{_{_{R} >}} & v^{∀,s} & < _{R} & w^{∃} \\ y^{∀,s} & < _{R} & x^{∃} & ^{∨^{U_{σ}}} & < _{E_{σ}} & u^{∃} \end{aligned}

and then to

\begin{aligned}x^{∃} & \overline{>} & • & \overline{>} & v^{∀,s} & \underline{<} & w^{∃} \\ y^{∀,s} & \underline{<} & • & ∨ & \underline{<} & u^{∃} \end{aligned}

representing the strong σ-update of R in the alternative sense.

Note that we have spared no efforts and included the treatment in case of the alternative definitions of [strong] existential R-substitution and σ-update in all our proofs!

Note 9: For 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.

Note 10: The other reason is that we do not have to insert R⟨{z^{∀,s}}⟩ × {y^{∀,s}} into the variable-condition R anymore (as was the case in Wirth (1998a) and Wirth (1998b)) because the transitive closure now takes care of this.

Note 11: Note that in Wirth (1998a) and Wirth (1998b) this “some” was still an “all”. Cf. the discussion at the end of Section 5.1.

Note 12: Suppose to weaken the notion of strong reduction in the following definition: G_{0} quite-strongly (C, R)-reduces to G_{1} in A if for each strong existential (A, R)-valuation e: if G_{1} is (C, R)-strongly (e, A)-valid, then G_{0} is (C, R)-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) R-reduction 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 have a lemma application without weak but only with strong free universal variables. But the (really essential!) transitivity of reduction as given in Lemma 5.11(3) is not given for quite-strong reduction.

Note 13: Note that in Wirth (1998a) and Wirth (1998b) the (non-liberalized) δ-rules were no sub-rules of Expansion rule of the sequent calculus of Def. 5.15 because there was only one kind of free universal variables and the δ-rule had to use the same kind of free universal variables as the liberalized δ-rule, cf. the discussion on p. 25 of Wirth (1998a).

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

Note 15: For the alternative notions in Note 8, we have to deviate here in the following way: Moreover, as R′ is the strong σ-update of R, we have R′ = (_{V_{free}\dom(σ)}|id ∪ E_{σ} ∪ U_{σ})R = V_{free}\dom(σ)|R ∪ E_{σ}R ∪ U_{σ}R. Thus, (_{V_{free}\dom(σ)}|R ∪ E_{σ}R ∪ U_{σ}R ∪ S_{e′})^{+} is a wellfounded ordering, just like its subset

(_{V_{free}\dom(σ)}|R ∪ S_{e′}|_{V_{∃}\dom(σ)} ∪ S_{e′}E_{σ}R ∪ U_{σ}R)^{+}.

The alternative version of a variable-condition guarantees ran(R) ⊆ V_{∀}. Since dom(σ) ⊆ V_{∃}, additional steps with _{dom(σ)}|R must cause immediate termination; i.e.

(R ∪ S_{e′}|_{V_{∃}\dom(σ)} ∪ S_{e′}E_{σ}R ∪ U_{σ}R)^{+}

is a wellfounded ordering, too. As ran(E_{σ} ∪ U_{σ}) ⊆ V_{∃} and dom(S_{e′} ∪ U_{σ}) ⊆ V_{∀}

(R ∪ S_{e′}|_{V_{∃}\dom(σ)} ∪ S_{e′}E_{σ} ∪ U_{σ})^{+}

is a wellfounded ordering, which is equal to (R ∪ S_{e})^{+} by definition of S_{e}. \underline{Q.e.d. (Claim 4)}

Note 16: For the alternative notions in Note 8, we have to deviate here in the following way: As R′ is the strong σ-update of R, we have U_{σ}R^{+} = U_{σ}RR^{∗} = (U_{σ}R)(_{V_{∀}}|R)^{∗} ⊆ R′R′^{∗} = R′^{+}, the second equality step being due to ran(R) ⊆ V_{∀} for any variable-condition R in the alternative case. Similarly, _{V_{∀}}|(R^{+}) = (_{V_{∀}}|R)^{+} ⊆ R′^{+}. Thus z^{∀}R′^{+}y^{∀,s}. \underline{Q.e.d. (Claim 3)}

Note 17: For the alternative notions in Note 8, we have to deviate here in the following way: As R′ is the strong σ-update of R, we have (_{V_{∃}\dom(σ)}|id ∪ E_{σ})R^{+} = (_{V_{∃}\dom(σ)}|id ∪ E_{σ})RR^{∗} = ((_{V_{∃}\dom(σ)}|id ∪ E_{σ})R)(_{V_{∀}}|R)^{∗} ⊆ R′R′^{∗} = R′^{+}, the second equality step being due to ran(R) ⊆ V_{∀} for any variable-condition R in the alternative case. Thus u^{∃}R′^{+}y^{∀,s}. Q.e.d. (Claim 4)

Note 18: For the alternative notions in Note 8, we have to deviate here in the following way: As R′ is the strong σ-update of R, we have R′ = (_{V_{free}\dom(σ)}|id ∪ E_{σ} ∪ U_{σ})R = V_{free}\dom(σ)|R ∪ E_{σ}R ∪ U_{σ}R. Thus, (_{V_{free}\dom(σ)}|R ∪ E_{σ}R ∪ U_{σ}R ∪ S_{e′} ∪ S_{π})^{+} is a wellfounded ordering, just like its subset

(_{V_{free}\dom(σ)}|R ∪ S_{e′}|_{V_{∃}\dom(σ)} ∪ S_{e′}E_{σ}R ∪ U_{σ}R ∪ S_{π})^{+}.

The alternative version of a variable-condition guarantees ran(R) ⊆ V_{∀}. Since ran(S_{π}) ⊆ V_{∀} and dom(σ) ⊆ V_{∃}, additional steps with _{dom(σ)}|R must cause immediate termination; i.e.

(R ∪ S_{e′}|_{V_{∃}\dom(σ)} ∪ S_{e′}E_{σ}R ∪ U_{σ}R ∪ S_{π})^{+}

is a wellfounded ordering, too. As ran(E_{σ} ∪ U_{σ}) ⊆ V_{∃} and dom(S_{e′} ∪ U_{σ} ∪ S_{π}) ⊆ V_{∀}

(R ∪ S_{e′}|_{V_{∃}\dom(σ)} ∪ S_{e′}E_{σ} ∪ U_{σ} ∪ S_{π})^{+}

is a wellfounded ordering, which is equal to (R ∪ S_{e} ∪ S_{π})^{+} by definition of S_{e}. Q.e.d. (Claim 3)

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.