1: Introduction

Section 1: Introduction

Most theorem proving paradigms for classical logic are centered around ad hoc proof structures which are designed to support a particular search procedure. Proof structures, such as resolution refutations or connection graphs, are not intended to be first-class values: they are very large, implementation dependent structures which are generally discarded after their discovery. This is very unfortunate since there is much information which could automatically be extract from such proofs. Such theorem provers are, for example, incapable of rendering natural justifications of their proofs to a human reader.

One obvious solution to this situation is to represent proofs by natural deduction or sequential proof trees. Such proof structures have been extensively studied and many structural manipulations are known. There are, however, at least two drawbacks to using such proof trees in a classical logic setting. First, such trees are also very large and awkward objects because they contain far more explicit information than is generally of interest. For example, natural deduction proofs record the order in which every logical connective and quantifier is introduced and eliminated. Secondly, Herbrand’s Theorem states that it is substitution which is the key element in classical proofs; logical connectives play a secondary and simplier role. Hence, it should be possible to greatly simplify representation of proofs in classical logic by simply recording the role substitutions play in building proofs.

In this paper, we present just such a representation for classical proofs, called expansion tree proofs. These proof structures record in a very compact form the essential information, namely substitutions, of classical proofs. We feel that these structures make suitable values within computational settings, and we demonstrate this by presenting several computations which can be performed directly on them. In particular, we show how to convert expansion tree proofs to H-proofs [8] (derivations from tautologies using universal and existential generalization), cut-free sequential proofs [7, 13, 16], and linear reasoning [5]. In the latter system, when interpolants exist, a very simple computation on expansion tree proofs will produce them. Finally, since many classical logic proof systems are designed to use Skolem terms to simplify the role of quantifiers in proofs, we present a version of expansion trees which use Skolem terms. We show that these two version are equivalent by presenting the transformations between them.

For traditional theorem proving systems, the conversion of expansion tree proofs to sequential proofs is very valuable. In particular, if a given resolution-style theorem prover built an expansion tree from its resolution refutation, the transformation to the “natural” proof structures described in Section 4 would provide a means by which a human readable presentation of a resolution refutation could be generated. Just such a practical use of expansion tree proofs has been demonstrated in [6, 11].

2: Logical Preliminaries

Since substitutions are central to understanding classical proofs and since the λcalculus is an elegant formalism for representing substitutions, we have choose to use a version of classical logic which is based on Church’s Simple Theory of Types [3]. This logic can represent quantification at all finite types, and, hence, all the results of this paper are valid for higher-order logic as well as for first-order logic. Furthermore, we have been able to provide two results for this higher-order logic which have not appeared before in the literature: a strengthened form of the (first-order) interpolation theorem, and a correct description of Skolem functions and the Herbrand Universe. Section 2: Logical Preliminaries

The higher-order logic, T , which we shall consider here is essentially the Simple Theory of Types described by Church in [3], except that we do not use the axioms of extensionality, choice, descriptions, or infinity. T contains two base types, o for boolean and ι for individuals, although adding any number of other base types can easily be done. All other types are functional types, i.e. the type (βα) is the type of a function with domain type α and codomain type β. Such types are often written elsewhere as α → β. The type (oα), being the type of a function from type α to booleans, i.e. a characteristic function, is used in T to represent the type for sets and predicates of elements of type α. Formulas are built up from logical constants, variables, and parameters (nonlogical constants) by λabstraction and function application. Hence, the type of [λx_{α}A_{β}] (where x_{α} is a variable) is (βα) while the type for [A_{(βα)}B_{α}] is β. (Here, type subscripts provide for type assignments.) We shall seldom adorn formulas with type symbols, but rather, when the type of a formula, say A, cannot be determined from context, we will add the phrase “where A is a formula_{α} (variable_{α}) (constant_{α})” to indicate that A has type α. When we do provides types as subscripts within larger formulas, we shall only provide an explicit type for the first occurrence of a variable or constant — we shall assume that all other occurrences will be implicitly typed the same. The logical constants of T are ∼_{oo} (negation), ∨_{(oo)o} (disjunction), and, for each type α, ∀_{o(oα)} (the “universal α-type set recognizer”). We also use the following abbreviations: A ∧ B stands for ∼[∼A ∨ ∼B], A ⊃ B stands for ∼A ∨ B, ∀x P stands for ∀[λxP], and ∃x P stands for ∼∀[λx ∼P]. Since the type of a set is of the form (oα), we write L_{oα}x_{α} to denote the set-theoretic expression x ∈ L.

We shall present a few simple facts about λ-conversion. The reader is referred to [3] and [4] for more details. If x is a variable_{α} and t is a formula_{α}, .S_{t}^{x}A denotes the formula which is the result of replacing all free occurrences of x in A with t. We shall assume that bound variable names are systematically changed to avoid variable capture. The operation of replacing a subformula of A of the form [λxC]E with .S_{E}^{x}C is called λ-contraction. We write A red B if B is the result of zero or more alphabetic changes in bound variables and λ-contractions of A. The converse of λ-contraction is λ-expansion. We write A conv B and say that A is λ-convertible to B if B is the result of zero or more alphabetic changes in bound variables, λ-contractions, and λ-expansions. A formula is in λ-normal form if it contains no contractible part, i.e. a subformula of the form [λxC]E. For every typed λ-calculus formula A there is a formula B in λ-normal form such that A red B. By principle normal formula we shall mean a formula B such that for each subformula λxC of B, x is the first variable in alphabetical order which is not free in C. Clearly, for every formula A there is a unique principle normal formula B such that A red B. The left-most, non-bracket symbol of the principle normal form of a formula A is called the head of A.

Definition 2.1. Let A be a λ-normal formula_{o}. An occurrence of a subformula B in A is a boolean subformula occurrence if it is in the scope of only ∼ and ∨, or if A is B. A boolean subformula occurrence is either positive or negative, depending on whether it is in the scope of an even or odd number of occurrences of ∼. The head of A is either ∼, ∨, ∀, or a variable or parameter. A is an atom if its head is a variable or parameter, and a boolean atom (b-atom, for short) if its head is a variable, parameter, or ∀.

Definition 2.2. Let B be a boolean atom occurrence in the formula_{o} A. If the head of B is not a ∀, then we say that B is neutral. Otherwise, we say that B is existential if it is in the scope of an odd number of negations and universal if it is in the scope of an even number of negations.

Below we list the axioms and rules of inference for the logical calculus T . First the axioms:

(1) All propositional tautologies.

(2) ∀_{o(oα)}f_{oα} ⊃ fx_{α}

(3) ∀x_{α} [p ∨ f_{oα}x] ⊃ p ∨ ∀_{o(oα)}f The rules of inference are the following:

(1) λ-conversion: From A to infer B provided that A conv B.

(2) Substitution: From F_{oα}x_{α} to infer F_{oα}A_{α} provided that x_{α} is not a free variable of F_{oα}.

(3) Modus Ponens: From A ⊃ B and A to infer B.

(4) Generalization: From F_{oα}x_{α} to infer ∀_{o(oα)}F_{oα}, provided that x_{α} is not a free variable of F_{oα}.

Those axioms and rules of inference which contain the type variable α are considered schemata. We say that a formula_{o}, A, is a theorem of T , written ⊢_{T} A, if there is a list of formulas_{o}, A_{1}, …, A_{n} = A (n ≥ 1) such that for each i, 1 ≤ i ≤ n, A_{i} is either an axiom or is derived from one or two previous formulas by a rule of inference. The deduction theorem holds for T .

The axioms and inferences of T are different from those for a first-order system only in the inclusion of λ-conversion and the richer structure of formulas. These two extensions, however, substantially change the character of inferences. Consider the following example of the interaction between λ-contractions and the logical connectives in higher-order logic.

Let Y be a variable_{oι}, and let D and T be variables_{o(oι)}. If we are given the formula

∀D [DY ⊃ T Y]

and we wished to do a universal instantiation of this formula with the term λZ_{oι}[T Z ∧ ∀x_{ι} [Zx ⊃ Ax]], i.e. the term representing the set of all sets of individuals which are members of T and are subsets of A, we would then have

[λZ[T Z ∧ ∀x [Zx ⊃ Ax]]]Y ⊃ T Y.

A λ-normal form of this formula is then

[T Y ∧ ∀x [Y x ⊃ Ax]] ⊃ T Y.

The structure of this last formula is much more complex than that of the formula from which it was deduced, since it contains occurrences of logical connectives and quantifiers which are not present in the original formula. Also, Y now has the role of a predicate where this was not the case in the first formula. None of these structural changes can occur in first-order logic.

Also consider the problems of extending Herbrand’s Fundamental Theorem [8] to higher-order logic. In first-order logic, Skolem functions and prenex normal forms can be used to reduce theoremhood for any formula to theoremhood of a formula of the form ∃x_{1} … ∃x_{n} A(x_{1}, …, x_{n}) where A contains no quantifiers. Herbrand’s Theorem then states that this formula is a theorem if and only if there is a collection of n-tuples (t_{1}^{1}, …, t_{n}^{1}), …, (t_{1}^{m}, …, t_{n}^{m}) of substitution terms from the Herbrand Universe, such that the compound Herbrand instance A(t_{1}^{1}, …, t_{n}^{1}) ∨ … ∨ A(t_{1}^{m}, …, t_{n}^{m}) is tautologous. In the higher-order setting, there are two important problems with this formulation of Herbrand’s Theorem. The first is that the Herbrand Universe of terms can not be constructed as simply a free term algebra. The interaction between λ-abstraction and Skolem functions must be restricted. We avoid using Skolem functions entirely until this issue is clarified in Section 6.

The second, more difficult problem in extending the first-order version of Herbrand’s Theorem is that in higher-order logic, the result of substituting terms for quantified variables in a given formula may yield new quantifiers which were not in the original formula, and hence have not been provided with a substitution term. For example, A(t_{1}^{i}, …, t_{n}^{i}) may contain quantifiers even if A(x_{1}, …, x_{n}) did not. Some of these quantifiers could also contribute new Skolem functions to the Herbrand Universe which might be required in some other substitution term, say t_{1}^{j} for j ≠ i. None of these possibilities are anticipated by the first-order version of this theorem.

This form of Herbrand’s Theorem fails to generalize to higher-order logic because it relies on two normal forms — prenex normal form and Skolem normal form — neither of which are preserved under substitution and λ-contraction. Our generalization of compound Herbrand instances, called expansion trees, will abandon these normal forms.

3: Expansion Tree Proofs

Section 3: Expansion Tree Proofs

In this section, structures which generalize formulas are defined. These structures, called expansion trees, may contain logical connectives as well as the new connective +^{t}, where t is a formula. Informally, an expression of the kind ∀B +^{t_{1}} Q_{1} +^{t_{2}} … +^{t_{n}} Q_{n}, for n ≥ 0, represents the result of instantiating the quantified expression ∀B with the terms t_{i} to get the structure Q_{i}, i = 1, …, n. Such an expression represents a labeled, ordered tree in which the root, labeled with the formula ∀B, has n out-arcs, each labeled in left-to-right fashion with the formulas t_{1}, …, t_{n}, which connect the root to the structures Q_{1}, …, Q_{n}. Such structures which contain no labeled arcs are interpreted as formulas_{o}.

Definition 3.1. Expansion trees, dual expansion trees, selected variables, expansion terms, and two functions Sh and Dp (for shallow and deep, resp.) which both map expansion trees and dual expansion trees to formulas are defined by the following mutual recursion.

(1) Let A be a λ-normal b-atom. If A is of the form ∀B then A is a dual expansion tree, otherwise it is both an expansion tree and a dual expansion tree. In either case, Sh(A) := A and Dp(A) := A.

(2) If Q is an expansion tree, then ∼Q is a dual expansion tree. If Q is a dual expansion tree, then ∼Q is an expansion tree. In either case, Sh(∼Q) := ∼Sh(Q) and Dp(∼Q) := ∼Dp(Q).

(3) Assume that Q_{1} and Q_{2} do not share selected variables. If Q_{1} and Q_{2} are expansion trees then so is Q_{1} ∨ Q_{2}. If Q_{1} and Q_{2} are dual expansion trees then so is Q_{1} ∨ Q_{2}. In either case Sh(Q_{1} ∨ Q_{2}) := Sh(Q_{1}) ∨ Sh(Q_{2}) and Dp(Q_{1} ∨ Q_{2}) := Dp(Q_{1}) ∨ Dp(Q_{2}).

(4) If Q is an expansion tree and Sh(Q) is a λ-normal form of By for some λ-normal formula_{oα} B and some variable_{α} y which is not selected in Q, then Q′ := ∀B +^{y} Q is an expansion tree. The variable y is a selected variable of Q′. Also, Sh(Q′) := ∀B and Dp(Q′) := Dp(Q).

(5) Let B be a λ-normal formula_{oα} and let t_{1}, …, t_{n} be a list of λ-normal formulas_{α} (n ≥ 1). If Q_{1}, …, Q_{n} is a list of dual expansion tree where no variable occurs selected more than once in all these trees, and for each i = 1, … n, Sh(Q_{i}) is a λ-normal form of Bt_{i}, then Q′ := ∀B +^{t_{1}} Q_{1} +^{t_{2}} … +^{t_{n}} Q_{n} is a dual expansion tree. The formulas t_{1}, …, t_{n} are expansion terms of Q′. Also, Sh(Q′) := ∀B and Dp(Q′) := Dp(Q_{1}) ∧ … ∧ Dp(Q_{n}).

It is very natural to think of both expansion trees and dual expansion trees as finite, ordered trees in which non-terminal nodes are labeled with either ∼, ∨, or ∀B, for some formula_{oα}, B, and where terminal nodes are labeled with b-atoms. A non-terminal node labeled with a formula of the form ∀B will also have out-arcs labeled with either occurrences of expansion terms or selected variables. These trees are viewed with their roots at the top and their leaves (terminal nodes) at the bottom. A node dominates another node if both are on a common branch and the first node is higher in the tree than the second. Arcs can dominate other arcs in the same fashion. This dominance relation will be considered reflexive. Also, an arc dominates a node if the node which terminates the arc dominates the given node. In particular, an arc dominates the node in which it terminates. Just as it is possible to classify subformula_{o} occurrences of formulas_{o} as either positive or negative, nodes in an expansion tree are classified as either positive if it is dominated by an even number of occurrence of ∼, or negative otherwise.

Definition 3.2. Let Q be either an expansion tree or a dual expansion tree, and let N be a node in Q which is labeled with ∀B for some formula_{oα} B. If Q is an expansion tree (dual expansion tree) then N is universal if it occurs positively (negatively) in Q and existential if it occurs negatively (positively) in Q.

In either an expansion tree or a dual expansion tree, a non-terminal node N labeled with a formula of the form ∀B is an instantiated node which is instantiated by the formulas labeling its out-arcs. It is easy to see that universal nodes are instantiated by selected variable and that existential nodes can only be instantiated by expansion terms. In the first case, the node N is selected by the selected variable, and in the second case N is expanded by the expansion terms. A universal (existential) node which is not dominated by any other universal or existential node is called a top-level universal (existential) node. A labeled arc is a top-level labeled arc if it is not dominated by any other labeled arc.

Definition 3.3. Let Q be an expansion tree or a dual expansion tree. S_{Q} is the set of all selected variables in Q and Θ_{Q} is the set of occurrences of expansion terms in Q. Let x be a variable_{α} which is not selected in Q, and t a formula_{α}. .S_{t}^{x}Q is defined as the result of applying .S_{t}^{x} to (and then normalizing) all formulas labeling either arcs or nodes in Q. .S_{t}^{x}Q is an expansion tree (dual expansion) if Q is an expansion tree (dual expansion tree), and Sh( .S_{t}^{x}Q) conv .S_{t}^{x}Sh(Q) and Dp( .S_{t}^{x}Q) conv .S_{t}^{x}Dp(Q). Finally, a variable is new to Q if it has no occurrence in any formula which is a label in Q.

The following relation is needed for our definition of Herbrand instances since Skolem functions are not being used.

Definition 3.4. Let A be an expansion tree and let <_{Q}^{0} be the binary relation on Θ_{Q} such that t <_{Q}^{0} s if there exists a variable which is selected for a node dominated by t and which is free in s. <_{Q}, the transitive closure of <_{Q}^{0}, is called the dependency relation for Q.

ET-proofs, which are our generalization of tautologous, compound, Herbrand instances, is defined below.

Definition 3.5. An expansion tree or dual expansion tree is sound if the free variables of Sh(Q) are not selected in Q. An expansion tree Q is an expansion tree for A if Sh(Q) is a λ-normal form of A and Q is sound. An expansion tree is grounded if none of its terminal nodes are labeled with formulas of the form ∀B. An ET-proof is an expansion tree Q such that Dp(Q) is tautologous and <_{Q} is acyclic. An ET-proof is a grounded ET-proof if it is also a grounded expansion tree.

Sound expansion trees are those trees which are expansion trees for some formula. In particular, if Q is a sound expansion tree, then Q is an expansion tree for Sh(Q).

Example 3.6. Let A be the theorem ∃y ∀x [P x ⊃ P y]. A grounded ET-proof for A would be the tree Q given as:

[∃y ∀x [P x ⊃ P y]+^{u}[∀x [P x ⊃ P u] +^{v} [P v ⊃ P u]]
+^{v}[∀x [P x ⊃ P v] +^{w} [P w ⊃ P v]]].

Here, Dp(Q) = [P v ⊃ P u] ∨ [P w ⊃ P v], Θ_{Q} = {u, v}, and S_{Q} = {v, w}. The dependency relation is given by the pair u <_{Q} v. If u was used in place of w, <_{Q} would have been cyclic.

The following proposition is straightforward.

Proposition 3.7. Let B be a finite set of variables. If A has an ET-proof, then it has an ET-proof in which no selected variable is a member of B.

A common way to present Herbrand’s Theorem is to show that any theorem can be proved in a system which contains tautologies as axioms and universal and existential generalizations as the sole inference rules [5, 8]. In particular, let H be the following proof system. The axioms of H are instances of tautologies. The inference rules are the following: anti-prenexing, existential and universal generalization, λ-expansion, and existential contraction (i.e. replace a negatively occurring subformula ∀B ∧ ∀B with ∀B). The proof of the following theorem shows how to translate expansion tree proofs into H-proofs.

Theorem 3.8. If the formula_{o} A has an ET-proof then it has an H-proof.

ET-proofs can be seen as directly encoding an H-proof. To prove this requires the following definitions and lemmas, many of which will also be used in the following section.

Definition 3.9. A term t is admissible in Q if no variable free in t is contained in S_{Q}. Let Q be either an expansion tree or a dual expansion tree, and let N be a top-level, instantiated node in Q. A labeled out-arc of N can be eliminated in one of the following two ways.

(1) If N is a universal node, then it is the root of a subtree of Q of the form ∀B +^{y} Q_{1}. The tree which results by replacing this subtree by Q_{1} is the result of eliminating y from Q.

(2) If N is an existential node, then it is the root of a subtree Q_{0} := ∀B +^{t_{1}} Q_{1} + … +^{t_{n}} Q_{n}. If n = 1 and t_{1} is admissible in Q, then let Q′ be the result of replacing Q_{0} with Q_{1}. If n > 1 and for some i, 1 ≤ i ≤ n, t_{i} is admissible in Q, then let Q′ be the result of replacing Q_{0} with the tree

[∀B +^{t_{1}} Q_{1} + … +^{t_{i−1}} Q_{i−1} +^{t_{i+1}} Q_{i+1} + … +^{t_{n}} Q_{n}] ∧ Q_{i}.

If in the first case i := 1, then in either case, Q′ is the result of eliminating t_{i} from Q.

Lemma 3.10. If Q′ is the result of eliminating a top-level labeled arc from the expansion tree Q then

(1) if <_{Q} is acyclic, then so is <_{Q′},

(2) Dp(Q′) and Dp(Q) are truth-functionally equivalent,

(3) if Q is sound then Q′ is sound, and

(4) if Q is sound then Sh(Q) can be derived from Sh(Q′) by some combination of

rule from the proof system H. Proof. Proofs of (1) and (2) are straightforward. To prove (3), assume that Q is sound. If Q′ arises by eliminating a selected variable y ∈ S_{Q}, then Q′ must also be sound, since the selected variable y, which may now be free in Sh(Q′), is not selected in Q′. Otherwise, assume Q′ arises by eliminating an admissible expansion term t ∈ Θ_{Q} from Q. Sh(Q′) can be formed by replacing an existential b-atom ∀B with a λ-normal form of either ∀B ∧ Bt or Bt. Assume that Q′ is not sound. Then there must be some z ∈ S_{Q′} = S_{Q} which is free in Sh(Q′). But then z is free in t, which contradicts the fact that t was admissible. Hence, Q′ is sound. Thus, if Q is an ET-proof then so is Q′.

Let Q be sound, so by (3), Q′ is sound. If Q′ is the result of eliminating a top-level selected variable, then Sh(Q) follows from Sh(Q′) by universal generalization, λ-expansion and anti-prenexing. If Q′ is the result of eliminating a top-level admissible, expansion term, then Sh(Q) can be derived from Sh(Q′) by using λ-expansion, existential generalization, anti-prenexing, and, possibly, existential contraction. Hence, (4) is proved. ⊓ ⊔

Lemma 3.11. If the expansion tree Q has a labeled arc and <_{Q} is acyclic, then some top-level labeled arc can be eliminated. Proof. If Q has a top-level selected variable, then this arc can be eliminated. Assume that Q has no top-level instantiated universal nodes. Let t_{1}, …, t_{m} be the list of all the occurrences of top-level expansion terms of Q. Since <_{Q} is acyclic, this list must contains a <_{Q}-minimal element. It is easy to verify that such minimal elements are admissible and can, therefore, be eliminated. ⊓ ⊔

The proof of Theorem 3.8 can now be completed. Let Q be an ET-proof for A. The preceding lemmas guarantee the existence of a list of ET-proofs, Q_{1}, …, Q_{m}, such that Q_{1} = Q, Q_{m} contains no labeled arcs, and for 1 ≤ i < m, Q_{i+1} is the result of eliminating a top-level, labeled arc from Q_{i}. Clearly, Q_{m} (= Sh(Q_{m})) is actually a tautologous formula and therefore has a (one line) H-proof. By induction and Lemma 3.10 (4), Sh(Q_{0}) has an H-proof. Since A is derivable from Sh(Q_{0}) by λ-expansion, A has an H-derivation.

This last theorem demonstrates how information in an ET-proof can be eliminated to yield a simpler ET-proof. It is also possible to take two expansion trees and combine their information to make a single expansion tree which collects their information. Such combining is needed in the next section.

Definition 3.12. Let Q_{1} and Q_{2} be both either grounded expansion trees or grounded dual expansion trees such that Sh(Q_{1}) and Sh(Q_{2}) are equal up to alphabetic changes of bound variables. Assume that selected variables which label arcs not dominated by expansion terms are the same in both trees. All other selected variables of Q_{1} and Q_{2} will be assumed to be different. In each step of the following recursive definition of merging Q_{1} and Q_{2} to get Q_{3}, the following facts are easily verified.

(a) If Q_{1} and Q_{2} are expansion trees then Q_{3} is an expansion tree, Sh(Q_{1}) = Sh(Q_{2}) = Sh(Q_{3}), and [Dp(Q_{1}) ∨ Dp(Q_{2})] ⊃ Dp(Q_{3}) is tautologous.

(b) If Q_{1} and Q_{2} are dual expansion trees then Q_{3} is a dual expansion tree, Sh(Q_{1}) = Sh(Q_{2}) = Sh(Q_{3}), and Dp(Q_{3}) ⊃[Dp(Q_{1}) ∧ Dp(Q_{2})] is tautologous.

The following recursively describes how to construct the merge of trees Q_{1} and Q_{2}. (1) If Q_{1} is a one-node tree, then so is Q_{2}, and Q_{3} := Q_{1} is the merge of Q_{1} and Q_{2}.

(2) If Q_{1} = ∼Q′_{1} then Q_{2} = ∼Q′_{2}. If Q′_{3} is the merge of Q′_{1} and Q′_{2}, then Q_{3} := ∼Q′_{3} is the merge of Q_{1} and Q_{2}.

(3) If Q_{1} = Q′_{1} ∨ Q′′_{1} then Q_{2} = Q′_{2} ∨ Q′′_{2}. If Q′_{3} and Q′′_{3} are the result of merging Q′_{1} with Q′_{2} and Q′′_{1} with Q′′_{2}, then merging Q_{1} with Q_{2} yields Q_{3} := Q′_{3} ∨ Q′′_{3}.

(4) If the root of Q_{1} is a existential node then Q_{1} = ∀B_{1} +^{t_{1}} Q_{1}^{1} + … +^{t_{n}} Q_{1}^{n} and Q_{2} = ∀B_{2} +^{s_{1}} Q_{2}^{1} + … +^{s_{m}} Q_{2}^{m}, where B_{1} and B_{2} are equal up to alphabetic change of bound variables, t_{1}, …, t_{n}, s_{1}, …, s_{m} are formulas, and n, m ≥ 1. The result of merging Q_{1} and Q_{2} is then simply

Q_{3} := ∀B_{1} +^{t_{1}} Q_{1}^{1} + … +^{t_{n}} Q_{1}^{n} +^{s_{1}} Q_{2}^{1} + … +^{s_{m}} Q_{2}^{m}.

(5) If the root of Q_{1} is a universal node then Q_{1} = ∀B_{1} +^{y} Q′_{1} and Q_{2} = ∀B_{2} +^{y} Q′_{2} where B_{1} and B_{2} are equal up to alphabetic changes of bound variables. If Q′_{3} is the result of merging Q′_{1} and Q′_{2} then Q_{3} := ∀B_{1} +^{y} Q′_{3} is the result of merging Q_{1} and Q_{2}.

Lemma 3.13. Let A, B, and C be formulas_{o}. We then have the following:

(1) If A ∨ B has a grounded ET-proof and C ∨ B has a grounded ET-proof, then [A ∧ C] ∨ B has a grounded ET-proof.

(2) If A ∨ B ∨ B has a grounded ET-proof, then A ∨ B has a grounded ET-proof.

4: Sequential Proofs

Proof. Only the proof of (1) is given since the proof of (2) is similar and easier. Thus, assume that A ∨ B and C ∨ B have grounded ET-proofs Q_{1} ∨ Q_{2} and Q_{3} ∨ Q_{4}. These expansion trees can be picked so that Q_{1} and Q_{3} can be merged to obtain Q_{5} and that Q := Q_{5} ∨[Q_{2} ∧Q_{4}] contains no variable selected twice. Clearly, Q is a grounded expansion tree for S ∨ [A ∧ B]. Since Q_{1} ∨ Q_{2} and Q_{3} ∨ Q_{4} are ET-proofs, Dp(Q_{1}) ∨ Dp(Q_{2}) and Dp(Q_{3}) ∨ Dp(Q_{4}) are tautologous. By the facts noted in the definition of merging, [Dp(Q_{1})∨Dp(Q_{3})] ⊃ Dp(Q_{5}) is tautologous. Hence, so too is Dp(Q) = Dp(Q_{5})∨[Dp(Q_{2})∧ Dp(Q_{4})]. Finally, if the dependency relation for Q contains a cycle, it is easy to show that that cycle must appear in either Q_{1} ∨ Q_{2} or Q_{3} ∨ Q_{4}. Hence, the dependency relation for Q is acyclic, and Q is indeed a grounded ET-proof of [A ∧ C] ∨ B. ⊓ ⊔

Section 4: Sequential Proofs

Our higher-order version of the sequential calculus, called L, is very similar to the L-systems given in [7, 13, 16]. For convenience the succedent and antecedent of sequents will be multisets. The structural inference figures for L are listed in Figure 1 and the introduction inference figures for ∼ and ∨ are listed in Figure 2. Here, Γ and Θ denote (possibly empty) multisets of formulas_{o}.

Γ ⟶ Θ ; Thinning ; A, Γ ⟶ Θ  Γ ⟶ Θ ; Thinning ; Γ ⟶ Θ, A
A, A, Γ ⟶ Θ

Contraction

A, Γ ⟶ Θ

Γ ⟶ Θ, A, A

Contraction

Γ ⟶ Θ, A

Figure 1: Structural inference figures.

A, Γ ⟶ Θ  C, Γ ⟶ Θ ∨−IA
A ∨ C, Γ ⟶ Θ

\begin{aligned}Γ ⟶ Θ, A, C \\ & ∨−IS \\ Γ ⟶ Θ, A ∨ C \end{aligned}

\begin{aligned}Γ ⟶ Θ, A \\ & ∼−IA \\ ∼A, Γ ⟶ Θ \end{aligned}  \begin{aligned}A, Γ ⟶ Θ \\ & ∼−IS \\ Γ ⟶ Θ, ∼A \end{aligned}

Figure 2: Inference figures for introducing ∨ and ∼.

Figure 3 lists the inference figures for the introduction of ∀ and the use of λ-convertibility. Here, A conv A′. The inference figure ∀−IS must be restricted so that y is not free in any of the formulas in its lower sequent. An L-derivation is defined, in the usual fashion, to be a tree structure of instances of these inference figures. An L-derivation is said to be an L-proof of its root sequent (endsequent) if its leaves are all axioms, i.e. they are of the form A → A, where A is any formula_{o}. A formula B has an L-proof if → B is the root sequent of an L-proof.

\begin{aligned}A, Γ ⟶ Θ \\ & λ \\ A′, Γ ⟶ Θ \end{aligned}  \begin{aligned}Γ ⟶ Θ, A \\ & λ \\ Γ ⟶ Θ, A′ \end{aligned}

\begin{aligned}Bt, Γ ⟶ Θ \\ & ∀−IA \\ ∀B, Γ ⟶ Θ \end{aligned}  \begin{aligned}Γ ⟶ Θ, By \\ & ∀−IS \\ Γ ⟶ Θ, ∀B \end{aligned}

Figure 3: Inference figures for λ and ∀.

The transformation from ET-proofs to sequent proofs is based on q-sequents, which are structures

P_{1}, …, P_{r} → Q_{1}, …, Q_{s}

where {Q_{1}, …, Q_{r}} is a possibly empty multiset of expansion trees and {P_{1}, …, P_{r}} is a possibly empty multiset of dual expansion trees, and ∼P_{1} ∨ … ∨ ∼P_{r} ∨ Q_{1} ∨ … ∨ Q_{s} is an ET-proof. (The choice of how these multisets are enumerated is not important.) This ET-proof is the ET-proof associated with this q-sequent, and the sequent

Sh(P_{1}), …, Sh(P_{r}) → Sh(Q_{1}), …, Sh(Q_{s})

is the sequent associated with this q-sequent. Notice that if Q is an ET-proof for A then → Q is a q-sequent, and the associated sequent would be → A′, where A′ is a λ-normal form of A. A q-sequent is grounded if its associated ET-proof is grounded.

Now let Σ be a (possibly empty) multiset of dual expansion trees, and let Ω be a (possibly empty) multiset of expansion trees. The following statements are true for qsequents.

(1) If P_{1} ∨ P_{2}, Σ → Ω is a q-sequent then both P_{1}, Σ → Ω and P_{2}, Σ → Ω are q-sequents.

(2) If Σ → Ω, Q_{1} ∨ Q_{2} is a q-sequent then Σ → Ω, Q_{1}, Q_{2} is a q-sequent.

(3) If Σ → Ω, ∼P is a q-sequent then P, Σ → Ω is a q-sequent.

(4) If ∼Q, Σ → Ω is a q-sequent then Σ → Ω, Q is a q-sequent.

These facts can be considered q-inference figures and are represented as such in Figure 4.

The following facts about q-sequents follow easily from the property of elimination of top-level selected variables and expansion terms (see Proposition 3.10).

P_{1}, Σ ⟶ Ω  P_{2}, Σ ⟶ Ω ∨−IA_{q}
P_{1} ∨ P_{2}, Σ ⟶ Ω

\begin{aligned}Σ ⟶ Ω, Q_{1}, Q_{2} \\ & ∨−IS_{q} \\ Σ ⟶ Ω, Q_{1} ∨ Q_{2} \end{aligned}

\begin{aligned}Σ ⟶ Ω, Q \\ & ∼−IA_{q} \\ ∼Q, Σ ⟶ Ω \end{aligned} \begin{aligned}P, Σ ⟶ Ω \\ & ∼−IS_{q} \\ Σ ⟶ Ω, ∼P \end{aligned}

Figure 4: The q-analogs for the inference figures in Figure 2.

(1) If Σ → Ω, ∀B +^{y} Q is a q-sequent then Σ → Ω, Q is a q-sequent.

(2) If ∀B +^{t_{1}} P_{1}, Σ → Ω is a q-sequent and if t_{1} is admissible in the associated ETproof, then P_{1}, Σ → Ω is a q-sequent. Similarly, if [∀B +^{t_{1}} P_{1} + … +^{t_{n}} P_{n}], Σ → Ω (n > 1) is a q-sequent and t_{i} is admissible for some i, 1 ≤ i ≤ n, then

P_{i}, [∀B +^{t_{1}} P_{1} + … +^{t_{i−1}} P_{i−1} +^{t_{i+1}} P_{i+1} + … +^{t_{n}} P_{n}], Σ → Ω

is a q-sequent. Figure 5 shows the q-inference figures based on these relationships between q-sequents.

A q-derivation is a tree structure of q-sequents, each of whose nonterminal nodes are instances of one of these seven q-inference figures.

\begin{aligned}Σ ⟶ Ω, Q \\ & ∀−IS_{q} \\ Σ ⟶ Ω, ∀B +^{y} Q \end{aligned}  \begin{aligned}P_{1}, Σ ⟶ Ω \\ & ∀−IA_{q} \\ ∀B +^{t_{1}} P_{1}, Σ ⟶ Ω \end{aligned}

P_{i}, [∀B +^{t_{1}} P_{1} + … +^{t_{i−1}} P_{i−1} +^{t_{i+1}} P_{i+1} + … +^{t_{n}} P_{n}], Σ ⟶ Ω ∀−IA_{q}^{∗}

[∀B +^{t_{1}} P_{1} + … +^{t_{n}} P_{n}], Σ ⟶ Ω Figure 5: The q-analogs for the ∀ inferences figures.

Let the degree of a q-sequent be the number of nonterminal nodes labeled with ∨ or ∼ plus the number of selected variables and occurrences of expansion terms in its expansion trees and dual expansion trees. In all the q-inference figures in Figures 4 and 5, the upper qsequents have strictly smaller degree than the lower sequents. Thus, any q-sequent Σ → Ω can be placed at the root of a q-derivation where all its leaves are q-sequents with zero degree. Theorem 3.11 must be used to ensure that if any expansion terms are present in a q-sequent then at least one of them is admissible. The following theorem now follows easily.

Theorem 4.1. If A is a formula_{o} with a grounded ET-proof, then there is an L-derivation of the sequent → A. Proof. Let Q be a grounded ET-proof for A. From the above discussion, → Q is the end q-sequent of a q-derivation, Ξ_{q}, in which the leaves are q-sequents of zero degree and in which the only q-inference figures used are those in Figures 4 and 5. Below, Ξ_{q} is transformed into an L-derivation tree Ξ whose endsequent is → A′, where A′ is some λ-normal form of A, and whose leaves contain only atomic formulas.

For any q-inference figure in Ξ_{q} in Figure 4, replace it with the L inference figure obtained by replacing the upper and lower q-sequents with their associated sequent and dropping the “q” subscript from the name of the inference figure. Hence, if a q-inference figure in Ξ_{q} is ∨−IA_{q} then the corresponding figure is Ξ is

Sh(P_{1}), Sh(Σ) ⟶ Sh(Ω)  Sh(P_{2}), Sh(Σ) ⟶ Sh(Ω) ∨−IA
Sh(P_{1}) ∨ Sh(P_{2}), Sh(Σ) ⟶ Sh(Ω)

Here, Sh(Σ) and Sh(Ω) are the multisets whose elements are the shallow formulas of the trees in Σ and Ω, respectively.

Now consider the inference figures in Figure 5. For any occurrence of a ∀−IS_{q} inference figure in Ξ_{q}, place in Ξ the inference figures

Sh(Σ) ⟶ Sh(Ω), A′ λ

Sh(Σ) ⟶ Sh(Ω), By ∀−IS

Sh(Σ) ⟶ Sh(Ω), ∀B

where A′ is a λ-normal form of By. Similarly, for any occurrence of a ∀−IA_{q} inference figure in Ξ_{q}, place in Ξ the inference figures

A′, Sh(Σ) ⟶ Sh(Ω) λ

Bt_{1}, Sh(Σ) ⟶ Sh(Ω) ∀−IA

∀B, Sh(Σ) ⟶ Sh(Ω)

where A′ is a λ-normal form of Bt_{1}. Finally, for any occurrence of a ∀−IA_{q}^{∗} inference figure in Ξ_{q}, place in Ξ the inference figures

A′, ∀B, Sh(Σ) ⟶ Sh(Ω) λ

Bt_{i}, ∀B, Sh(Σ) ⟶ Sh(Ω) ∀−IA

∀B, ∀B, Sh(Σ) ⟶ Sh(Ω)

Contraction

∀B, Sh(Σ) ⟶ Sh(Ω)

where A′ is a λ-normal form of Bt_{i}.

Ξ is an L-derivation of → A′ (where A′ is a λ-normal form of A) in which the leaves are sequents containing only atoms. Let Ξ′ be the L-derivation which results from placing at the endsequent of Ξ the inference figure

⟶ A′ ; λ. ; ⟶ A

Each leaf of Ξ′ is a sequent of the form Γ → Θ in which Γ and Θ are multisets of atomic formulas_{o} and [∨∼Γ] ∨ [∨Θ] is tautologous. Thus Γ and Θ contain a common atomic formula, i.e. Γ → Θ is the result of thinning an axiom. Let Ξ′′ be the L-proof of → A which is constructed from Ξ′ by placing above each leaf of Ξ′ an axiom sequent and enough thinning inferences to infer that leaf. Ξ′′ is then an L-proof of → A. ⊓ ⊔

Now consider the converse of this theorem.

Theorem 4.2. If the sequent Γ → Θ has an L-proof, there is a grounded q-sequent Σ → Ω such that Γ = Sh(Σ) and Θ = Sh(Ω). Thus, if A has an L-proof, it has a grounded ET-proof. Proof. Assume that the sequent Γ → Θ has an L-proof Ξ. This L-proof can be assumed to have axioms which involve only λ-normal atomic formulas, since otherwise it could be reduced to such a proof by applying various inference figures to the non-atomic axioms. We prove by induction on the height of Ξ that there is a grounded q-sequent, Σ → Ω, such that Γ = Sh(Σ) and Θ = Sh(Ω).

If the height of Ξ is 0, then Ξ is an axiom instance, say C → C. If C′ is a λ-normal form of C, then C′ → C′ is the desired grounded q-sequent.

Now assume the height of Ξ is greater than 0. We need to show how a q-sequent for the final sequent of Ξ can be constructed from the q-sequent(s) associated with the premise(s) of that sequent. To do this, we need to consider 12 cases; one for each inference rule which may terminate the proof tree Ξ. The construction for most of these cases is very simple. For example, the q-sequent for the premise of either λ inference rule is also a q-sequent for its conclusion. For the ∀ introduction rules, the q-sequent for the conclusion is simply the result of adding a labeled arc and new root node to the q-sequent for the premise. It is only the contraction and ∨−IA rule where the construction is not immediate. Both these cases, however, were already anticipated and solved by Lemma 3.13.

Thus there is a quite simple inductive algorithm which can construct a ground qsequent for the root sequent of an L-proof. Hence, if Ξ is an L-proof of the sequent → A, this algorithm constructs a q-sequent, say → Q, such that Q is grounded and A red Sh(Q). Hence, Q is a grounded ET-proof for A. ⊓ ⊔

Another way to state the cut-elimination result for T is that for any formula_{o} A, ⊢_{T} A if and only if there is a (cut-free) proof of A in L. Using the above two theorems, the soundness and completeness for ET-proofs follows immediately, i.e. ⊢_{T} A if and only if A has a grounded ET-proof.

5: Linear Reasoning

The proof transformation algorithms presented in this section have very practical value for the implementation of theorem proving systems. If a resolution-style theorem prover recorded its substitution information in an expansion tree, the transformation from ET-proofs to L-proof could be used to constitute a “natural” rendering of a resolution refutation. Also, consider the following kind of theorem proving system: let a user interactively edit a sequent-style proof. Once a proof is completed, the transformation of L-proofs to ET-proofs could be applied. The resulting ET-proof would record just the “essential” information of the proof. If this latter ET-proof was to be transformed back to a sequential proof, there are many such proofs which could be produced: the orginal sequential proof is only one of many. If the sequential proof builder encompassed notions of good proof style, the newly created sequential proof could be a stylistically improved version of the orginally entered sequential proof. Such proof revision has been experimented with in [6].

Section 5: Linear Reasoning

If the formula C ⊃ D has an ET-proof, it is of the form P ⊃ Q, where P is a dual expansion tree for C and Q is an expansion tree for D. (For convenience, expansion trees shall be denoted by a (possibly) ornamented “Q” while a dual expansion tree shall be denoted by a (possibly) ornamented “P.”) As was shown in the proof of Theorem 3.8, there is a list of ET-proofs

P ⊃ Q = P_{1} ⊃ Q_{1}, …, P_{n} ⊃ Q_{n}

such that Dp(P_{n}) ⊃ Dp(Q_{n}) is tautologous, and for 1 ≤ i < n, either P_{i+1} is equal to P_{i} and Q_{i+1} is the result of eliminating a top-level labeled arc from Q_{i}, or Q_{i+1} is equal to Q_{i} and P_{i+1} is the result of eliminating a top-level labeled arc from P_{i}. In the first case, either ⊢_{T} Sh(Q_{i+1}) ⊃ Sh(Q_{i}) or ⊢_{T} ∀y Sh(Q_{i+1}) ⊃ Sh(Q_{i}), depending on whether Q_{i+1} is the result of eliminating an expansion term or a universal variable y from Q_{i}. In the latter case, either ⊢_{T} Sh(P_{i}) ⊃ Sh(P_{i+1}) or ⊢_{T} Sh(P_{i}) ⊃ ∃y Sh(P_{i+1}), depending on whether P_{i+1} is the result of eliminating an expansion term or a universal variable y from P_{i}. It is this relationship between Sh(P_{i}) and Sh(P_{i+1}) and between Sh(Q_{i+1}) and Sh(Q_{i}) which is the basis of Craig’s system of linear reasoning.

Let A be a formula_{o} and ψ be a (possibly empty) list of quantifier occurrences, ∀x or ∃x, for any variable x. We define a prefixed formula to be a pair ⟨ψ, A⟩, also written as ψA. A prefixed formula ⟨ψ, A⟩ represents the formula B if B is the result of attaching to A the quantifiers listed in ψ. While ⟨ψ, A⟩ represents a unique formula, the converse is not true. For example, the formula ∃x∀y P xy is represented by the three prefixed formulas ⟨∃x∀y, P xy⟩, ⟨∃x, ∀y P xy⟩, and ⟨∅, ∃x∀y P xy⟩.

Let A be a formula_{o} and let B be a boolean subformula occurrence in A. We will use the symbol A[B]^{±} to denote this fact. The symbol ± will be + if the occurrence of B is positive and will be − otherwise. Once the position and sign of an occurrence of B in A is established, that occurrence of B can be changed. This is done by using the symbol A[C]^{±}, i.e. the instance of B which was marked out in A[B]^{±} is now changed to C. The symbols A[B]^{±} and A[C]^{±} only make sense when they occur in pairs.

Below is the list of L-deductions used in linear reasoning. Each L-deduction takes one prefixed formula as a premise and yields one prefixed formula as a conclusion. Duplication: From ψ A[∀B]^{+} infer ψ A[∀B ∧ ∀B]^{+}. Simplication: From ψ A[∀B ∧ ∀B]^{−} infer ψ A[∀B]^{−}. ∃-exportation: From ψ A[∀B]^{−} infer ψ∃y A[By]^{−}. ∀-importation: From ψ∀y A[By]^{+} infer ψ A[∀B]^{+}, when y is not free in A[∀B]. ∀-vacuous-introduction: From ψ_{1}ψ_{2} A infer ψ_{1}∀yψ_{2} A. ∃-vacuous-removal: From ψ_{1}∃yψ_{2} A infer ψ_{1}ψ_{2} A, when y is not free in ψ_{2}A. ∃-generalization: From ψ A[Bt]^{−} infer ψ A[∀B]^{−}. ∀-instantiation: From ψ A[∀B]^{+} infer ψ A[Bt]^{+}. Matrix-change: From ψ A infer ψ A′, provided that A ⊃ A′ is tautologous. λ-conversion: From ψ A infer ψ A′, provided that A conv A′.

Notice that if ψ A, ψ′ A′ is a L-deduction then for any variable y, both ∀yψ A, ∀yψ′ A′ and ∃yψ A, ∃yψ′ A′ are justified by the same L-deduction. Furthermore, in the deductions ∀-instantiation, ∃-generalization, and matrix-change, the premise implies the conclusion. In all the remaining deductions, the premise is equivalent to conclusion. A list of prefixed formulas ψ_{1}A_{1} …, ψ_{n}A_{n} is called an L-derivation of ψ_{n}A_{n} from ψ_{1}A_{1} if for each i, 1 ≤ i < n, ψ_{i} A_{i}, ψ_{i+1} A_{i+1} is one of the above L-deductions. If B_{1} represents ψ_{1}A_{1} and B_{n} represents ψ_{n}A_{n}, then ⊢_{T} B_{1} ⊃ B_{n}. Definition 5.1. An L-derivation is balanced if there exists exactly one matrix-change deduction and all ∀-instantiations and Duplications occur before and all ∃-generalization and Simplications after this matrix-change, and all λ-conversions prior to the matrixchange are λ-contractions while all those after the matrix-change are λ-expansions. Given a balanced L-derivation there is a prefix ψ and two formulas_{o} M_{1} and M_{2} such that the L-deduction ψM_{1}, ψM_{2} is the matrix-change deduction for this L-derivation. We shall call ψ the matrix prefix, M_{1} the left matrix formula, and M_{2} the right matrix formula of this L-derivation. Theorem 5.2. If ⊢_{T} C ⊃ D then there is a balanced L-derivation of D from C. In fact, let P ⊃ Q be an ET-proof of C ⊃ D and let S be the set of selected variables of P ⊃ Q which are free in Dp(P ⊃ Q) and let ≺ be the embedding relation for P ⊃ Q. There is a balanced L-derivation of D from C such that its left and right matrix formulas are equal (modulo associativity of conjunction) to Dp(P) and Dp(Q), respectively, and its matrix prefix is

Q_{m}y_{m}, …, Q_{1}y_{1},

6: Skolemization

where y_{1}, …, y_{m} is a topological sort of S with respect to ≺ (i.e. if y_{i} ≺ y_{j} then i < j) and Q_{i} is ∃ if y_{i} is selected in the tree P and is ∀ if y_{i} is selected in the tree Q, for i = 1, …, m.

The proof of this theorem closely parallels the one given by Craig in [5]. There are two main differences, however. The first is the obvious addition of λ-formulas and λ-conversion. This complicates the nature of ∀-instantiation and ∃-generalization deductions and forces the second difference. Since the substitution of higher-order terms can result in the appearance of embedded quantifiers, formulas in an L-derivation cannot be required to be in prenex normal form. Dropping prenex normal forms, although necessary, does not make doing linear reasoning any harder. L-derivations cannot, however, be require to satisfy the property that any Duplication, ∃-exportation, and ∀-vacuous-introduction precedes any ∀-instantiation deduction and that any Simplication, ∀-importation, and ∃-vacuous-removal deduction follows any ∃-generalization deduction. Although this is possible in the first-order setting, here these various deductions may well need to get mixed on the left side (for the first four deductions) and the right side (for the second four deductions) of the matrix-change.

Let M_{1} and M_{2} be two formulas such that M_{1} ⊃ M_{2} is tautologous. From [5] it is easy to see that there is a third formula M such that both M_{1} ⊃ M and M ⊃ M_{2} are tautologous, and that every parameter or free variable occurring in M occurs in both M_{1} and M_{2}. Such a formula M is a propositional interpolant for M_{1} ⊃ M_{2}. The following weak interpolation theorem holds for T .

Theorem 5.3. If the closed formula C ⊃ D has an ET-proof P ⊃ Q then there exists a formulas X such that ⊢_{T} C ⊃ X, ⊢_{T} X ⊃ D, and if a parameter c occurs in X and not in both C and D, then c occurred either in D and some expansion term of P or in C and some expansion term of Q. Proof. Let P ⊃ Q be an ET-proof for C ⊃ D, M be a propositional interpolant for Dp(P) ⊃ Dp(Q), and ψ be the prefix described in Theorem 5.2. Then ψM is a formula such that ⊢_{T} C ⊃ ψM and ⊢_{T} ψM ⊃ D. The only parameters occurring in M must be in both Dp(P) and Dp(Q). Since the only parameters occurring in Dp(P) occur in either C or expansion terms of P and the only parameters occurring in Dp(Q) occur in either D or an expansion term of Q, ψM satisfies the conditions of the theorem. ⊓ ⊔

This theorem can be viewed as an extension of the interpolation theorem for first-order logic since it immediately yields that theorem: Since expansion terms in first-order logic can not contain predicates, the predicates in the formula ψM must be common to both C and D, no matter which ET-proof was used to construct ψM.

Section 6: Skolemization

The nature of Skolem functions in higher-order logic is more complex than it is for first-order logic. In first-order logic, the Herbrand Universe of terms is freely generated from Skolem functions using application. Terms containing Skolem functions can be used identical to terms not containing Skolem functions. In higher-order logic, however, the use of Skolem functions must be modified. For example, the formula

∀x_{ι} ∃y_{ι} P_{(oι)ι}xy ⊃ ∃f_{ιι} ∀z_{ι} P z[fz]

is not provable in T , although the following Skolemized form of it is provable:

∀x_{ι} P_{(oι)ι}x[gx] ⊃ ∃f_{ιι} P [hf][f[hf]].

Here, g is a Skolem function_{ιι} and h is a Skolem function_{ι(ιι)}. If such functions are not restricted, this latter formula would have an ET-proof in which f would be substituted with either g or λx gx. The lack of such a restriction in the resolution refutation system in [1] caused that system to be unsound. Assuming the Axiom of Choice would have made that refutation system sound but then not complete.

Skolem functions should simply play the syntactic role of providing for a parametric collection of new “objects.” They should not be used as an actual function such as g is when used in the substitution terms g and λx gx in the above example. The necessary restriction on Skolem functions is given in the following definition.

Definition 6.1. The list σ := ⟨α, β_{1}, …, β_{p}⟩, where α, β_{1}, …, β_{p} are type symbols (p ≥ 0), is called a signature (for a Skolem function). For each signature, σ, let K_{σ} be a denumerably infinite set of function symbols all of type (… (αβ_{1}) … β_{p}) which are not in the formulation of T and such that if σ_{1} and σ_{2} are two different signatures then K_{σ_{1}} and K_{σ_{2}} are disjoint. f ∈ K_{σ} is called a Skolem function of signature σ with arity p. Let T^{∗} be the formulation of T in which these Skolem functions are added. The Herbrand Universe of terms for T^{∗} is the set, U, of all formulas A of T^{∗} such that whenever a Skolem function of arity p has an occurrence in A, it is applied to at least p arguments. These arguments are called its necessary arguments, and a formula with a Skolem function of arity p with p argument attached is called a Skolem term. Furthermore, if a variable has a free occurrence in any of these necessary arguments, that occurrence is also free in A. U_{α} will denote the set of all formulas in U of type α.

Two Skolem functions may have the same type while they have different arities. For example, if α is of the form α′β_{0}, then a Skolem term with signature ⟨α, β_{1}, …, β_{p}⟩ and one with the signature ⟨α′, β_{0}, β_{1}, …, β_{p}⟩ have different arities but have the same type. Since types can generally be determined from context while arity often cannot be, Skolem functions are frequently written with a superscripted nonnegative integer to denote its arity, i.e. f^{p}.

Example 6.2. If f, g are Skolem terms with signature ⟨ι, ι⟩, x, w are variables_{ι}, and A is a variable_{o(oι)} then f[gx] ∈ U_{ι}, λxx ∈ U_{ιι}, and λw[Aw[gx]] ∈ U_{oι}, while f ∉ U, λx[fx] ∉ U, and λw[A[gx][fw]] ∉ U.

The following proposition can easily be established using standard methods of the λ-calculus.

Proposition 6.3. If A ∈ U_{α} and A red B then B ∈ U_{α}.

Expansion trees can now be modified to use Skolem functions in place of selected variables.

Definition 6.4. Skolem expansion trees and dual Skolem expansion trees are defined similarly to expansion trees and dual expansion trees, except as follows. When building trees, Skolem terms are used to instantiate universal nodes in place of selected variables. Second, expansion terms must be members of U. Finally, there are two global requirements. Let f^{p}t_{1} … t_{p} be the Skolem term which labels the sole out-arc of a universal node, N. Then f^{p} appears as the head of no other Skolem term labeling the out arc of universal node. Also, on the path from N to the root of the tree, there are exactly p expansion terms t_{1}, …, t_{p}, in that order of dominance, which dominate N. The term f^{p}t_{1} … t_{p} is said to be used to do a Skolem instantiation of the node N.

The definitions for the functions Dp and Sh are essentially the same as they are presented in Definition 3.1. A Skolem expansion tree, Q, is a tree for a formula A of T if Sh(Q) conv A and Q is an ST-proof if Dp(Q) is tautologous.

There are two fundamental differences between expansion trees and Skolem expansion trees: First, subtrees of expansion trees are either expansion trees or dual expansion trees, while subtrees of Skolem expansion trees are not necessarily Skolem expansion trees or their duals. Second, a substitution instance of a Skolem expansion tree is another Skolem expansion tree, while the substitution instance of an expansion tree with an acyclic dependency relation may no longer be an expansion tree with an acyclic dependency relation. This fact is the main reason why proof structures using Skolemization are frequently used in automated proof systems. It is important in many of these automated systems that proof systems remain proof systems under substitution.

Example 6.5. Let A be the theorem ∃y ∀x [P x ⊃ P y], and let f and g be Skolem functions with signature ⟨ι, ι⟩. A Skolem expansion tree for A would then be the tree Q_{1} given as (compare with Example 3.6):

[∃y ∀x [P x ⊃ P y]+^{u}[∀x [P x ⊃ P u] +^{fu} [P [fu] ⊃ P u]]
+^{v}[∀x [P x ⊃ P v] +^{gv} [P [gv] ⊃ P v]]].

An ST-proof for A would then be the tree Q_{2} given as:

[∃y ∀x [P x ⊃ P y]+^{u}[∀x [P x ⊃ P u] +^{fu} [P [fu] ⊃ P u]]
+^{v}[∀x [P x ⊃ P v] +^{g[fu]} [P [g[fu]] ⊃ P [fu]]]].

Q_{2} is the result of substituting fu for v in Q_{1}.

The definition of ST-proofs has no condition similar the one for ET-proofs which required the dependency relation be acyclic. The restriction it specified for ET-proofs is explicitly encoded into Skolem terms used in ST-proofs. To make this relationship more explicit, the following binary relation for the selected variables in expansion trees is provided.

Definition 6.6. Let Q be an expansion tree. Let ≺_{Q}^{0} be the binary relation on S_{Q} such that z ≺_{Q}^{0} y if there exists a t ∈ Θ_{Q} such that z is free in t and a node dominated by (the arc labeled with) t is selected by y. ≺_{Q}, the transitive closure of ≺_{Q}^{0}, is called the embedding relation.

This relation is closely related to the dependency relation. The following proposition and its proof reveals this connection.

Proposition 6.7. <_{Q} is acyclic if and only if ≺_{Q} is acyclic. Proof. Let <_{Q} be cyclic. That is, assume that there are expansion term occurrences t_{1}, …, t_{m} ∈ Θ_{Q} such that t_{1} <_{Q}^{0} … <_{Q}^{0} t_{m} <_{Q}^{0} t_{m+1} = t_{1} for m ≥ 1. Let y_{i}, for i = 1, …, m, be chosen from S_{Q} so that y_{i} is selected for a node dominated by t_{i} and y_{i} is free in t_{i+1}. If y_{m+1} is identified with y_{1}, then y_{i} ≺_{Q}^{0} y_{i+1}, for i = 1, …, m, since y_{i+1} is selected for a node dominated by t_{i+1} and y_{i} is free in the formula t_{i+1}. Hence, y_{1} ≺_{Q}^{0} … ≺_{Q}^{0} y_{m} ≺_{Q}^{0} y_{1}, and ≺_{Q} is cyclic. The proof in the other direction is very similar. ⊓ ⊔

As will be shown, an ET-proof Q can be converted to an ST-proof Q′, and conversely. In such a case, two selected variables z and y of Q satisfy z ≺_{Q} y if and only if the Skolem term corresponding to z is a subformula of the Skolem term corresponding to y. Since the subformula relation is guaranteed to be acyclic, it is not necessary to assume any additional acyclic conditions for ST-proofs.

Theorem 6.8. If A has an ET-proof then A has an ST-proof. Proof. Let A have an ET-proof Q. For any selected variable_{α} y ∈ S_{Q} define an associated Skolem term as a term ft_{1} … t_{p}, such that (a) t_{1}, …, t_{p} are the expansion terms in Q which dominate the arc labeled with y, (b) these expansion terms are ordered so that 1 ≤ l < k ≤ p implies t_{l} dominates t_{k}, and (c) f is some Skolem function with signature ⟨α, β_{1}, …, β_{p}⟩, where β_{j} is the type of t_{j}, j = 0, …, p. Since none of the formulas, t_{1}, …, t_{p} contain Skolem functions, associated Skolem terms are all members of U.

Let ⟨y_{1}, …, y_{r}⟩ be a list of the variables in S_{Q} such that y_{i} ≺_{Q} y_{j} implies i < j, and let ⟨s_{1}, …, s_{r}⟩ be a corresponding list of associated Skolem terms all of which have different Skolem functions for their heads. Notice that 1 ≤ i ≤ j ≤ r implies that y_{j} is not free in s_{i}.

Let φ := .S_{s_{1}}^{y_{1}} ∘ ⋯ ∘ .S_{s_{r}}^{y_{r}}. A simple induction argument shows that if C is a formula of T , then φC will be a formula of T^{∗} in which none of the variables y_{1}, …, y_{r} are free.

Also, φy_{i} is a Skolem term with top-level Skolem function f_{i}. It is easy to verify that φ commutes with Dp, Sh, and +^{t}. From this it follows immediately that φQ is an ST-proof for A. ⊓ ⊔

To convert ST-proofs to ET-proofs, Skolem terms must be replaced with selected variables. The following operator is used to do this.

Definition 6.9. Let A ∈ U_{α}, s be a Skolem term_{β}, and y be a variable_{β} which does not appear in A or in s. Let D_{y}^{s}A, the deskolemizing operator, be the result of replacing in A every subformula, t, such that t conv s, by y. If Q is a Skolem expansion tree, then D_{y}^{s}Q is the result of applying D_{y}^{s} to all formulas labeling arcs and nodes in Q.

Example 6.10. If f be a Skolem function with signature ⟨ιι, ι⟩, then

D_{y}^{fv}[λz_{ι}[fv_{ι}z]] = λz[y_{ιι}z] and D_{y}^{fv}P z[f[[λw_{ι} w]v]] = P zy.

The following proposition can be proved using standard methods of λ-calculus.

Lemma 6.11. Let A, B ∈ U_{α}, s be a Skolem term_{β}, and y be a variable_{β} which does not appear in A, B, or s. The all the following are true.

(1) D_{y}^{s}A ∈ U_{α} and .S_{y}^{s}D_{y}^{s}A conv A.

(2) A red B implies D_{y}^{s}A red D_{y}^{s}B.

(3) If B is a λ-normal form of A, then D_{y}^{s}B is a λ-normal form of D_{y}^{s}A. The soundness of Skolem functions is proved by the following theorem.

Theorem 6.12. If A has an ST-proof then A has an ET-proof. Proof. Let Q be an ST-proof for A and let V be the set of principle normal forms of Skolem terms which are subformulas of formulas used to do expansions or Skolem instantiations in Q. Let ⟨s_{1}, …, s_{r}⟩ be an ordering of V such that whenever s_{j} is an alphabetic variant of a subformula of s_{i} then i < j. Let y_{1}, …, y_{r} be r distinct variables new to Q and A such that y_{i} has the same type as s_{i}, i = 1 …, r. Let ρ be the compound deskolemizing operator

ρ := D_{y_{n}}^{s_{n}} ∘ ⋯ ∘ D_{y_{1}}^{s_{1}}.

Now ρs_{i} = y_{i}, for all i = 1, …, r, since j < i implies that D_{y_{j}}^{s_{j}}s_{i} = s_{i}. By Lemma 6.11, it is easy to see that ρ commutes with Dp, Sh, and +^{t}. Since Sh(Q) contains no Skolem functions, Sh(ρQ) = Sh(Q). Hence, ρQ is an expansion tree for A. We need only show that ≺_{ρQ} is acyclic.

Assume that y_{i} ≺_{ρQ}^{0} y_{j} for some y_{i}, y_{j} ∈ S_{ρQ}. Then the selection arc labeled with y_{j} in ρQ is dominated by some expansion term t which contains a free occurrence of y_{i}. Let t′, s′_{j}, s′_{i} be the formula labeling the arcs in Q which correspond to the arc labeled with t, y_{j}, y_{i}, respectively, in ρQ. Here, the principle normal form of s′_{j} and s′_{i} are s_{j} and s_{i}, respectively. Clearly, t′ would contain s′_{i} as a subformula, while t′ is a subformula of s′_{j}. Thus s_{i} is an alphabetic variant of a subformula of s_{j} and, therefore, j < i. Therefore, if y_{i} ≺_{ρQ} y_{j} then j < i, and ≺_{ρQ} is acyclic. ⊓ ⊔

The soundness and completeness for ST-proofs follow immediately from the above two theorems.

Acknowledgements

Much of the material presented here was taken from my dissertation done in the Mathematics Department at Carnegie-Mellon University. This thesis, titled “Proofs in Higher-Order Logic,” is available as technical report MS-CIS-83-37 from the Computer and Information Science Department, University of Pennsylvania. I am greatly indebted to Peter Andrews, my dissertation advisor, for my formal training in logic and for a good deal of encouragement. I was also helped by numerous conversations with Frank Pfenning, Rick Statman, Daniel Leivant, and Dana Scott. I would also like to thank Gopalan Nadathur, Dafa Li, and Greg Hager for their comments on an early draft of this paper. This research was supported by NSF grant MCS81-02870.

Bibliography

[1] Peter B. Andrews, Resolution in Type Theory, Journal of Symbolic Logic 36 (1971), 414 – 432.

[2] Peter B. Andrews, Dale A. Miller, Eve Longini Cohen, Frank Pfenning, “Automating Higher-Order Logic” in Automated Theorem Proving: After 25 Years, AMS Contemporary Mathematics Series 29 (1984).

[3] Alonzo Church, A Formulation of the Simple Theory of Types Journal of Symbolic Logic 5 (1940), 56 – 68.

[4] Alonzo Church, The Calculi of Lambda-Conversion, Princeton University Press, 1941.

[5] William Craig, Linear reasoning. A new form of the Herbrand-Gentzen theorem, Journal of Symbolic Logic 22 (1957), 250 – 268.

[6] Amy P. Felty, “Using Extended Tacticals to Do Proof Transformations,” MSE Thesis, University of Pennsylvania, December 1986.

[7] Gerhard Gentzen, Investigations into Logical Deductions in The Collected Papers of Gerhard Gentzen edited by M. E. Szabo, North-Holland Publishing Co., Amsterdam, 1969, 68 – 131.

[8] J. Herbrand, Recherches sur la théorie de la démonstration, Travaux de la Société des Sciences et des Lettres de Varsovie, Classe III Sciences Mathematiques et Phyiques 33 (1930). Translated in [9].

[9] J. Herbrand, Logical Writings, Harvard University Press, Cambridge, Mass, 1972.

[10] Gérard P. Huet, “A Mechanization of Type Theory,” Proceedings of the Third International Joint Conference on Artificial Intelligence 1973, 139 – 146.

[11] Dale A. Miller, “Expansion Tree Proofs and Their Conversion to Natural Deduction Proofs,” 7th International Conference on Automated Deduction (ed. by R. E. Shostak), Springer-Verlag, LNCS 170, 375 –393.

[12] Tomasz Pietrzykowski, “A Complete Mechanization of Second-Order Type Theory,” Journal of the Association for Computing Machinery 20 (1973), 333 – 364.

[13] Dag Prawitz, Natural Deduction, Almqvist & Wiksell, 1965.

[14] Dag Prawitz, Hauptsatz for higher order logic, Journal of Symbolic Logic 33 (1968), 452 – 457.

[15] J. A. Robinson, “Mechanizing Higher-Order Logic,” Machine Intelligence 4, Edinburgh University Press, 1969, 151 – 170.

[16] Raymond M. Smullyan, First-Order Logic, Springer-Verlag, New York, 1968.

[17] Moto-o-Takahashi, A proof of cut-elimination theorem in simple type-theory, Journal of the Mathematical Society of Japan 19 (1967), 399 – 410.

A Compact Representation of Proofs

Dale A. Miller Computer and Information Science University of Pennsylvania Philadelphia, PA 19104-6389, USA 23 February 1993

Abstract: A structure which generalizes formulas by including substitution terms is used to represent proofs in classical logic. These structures, called expansion trees, can be most easily understood as describing a tautologous substitution instance of a theorem. They also provide a computationally useful representation of classical proofs as first-class values. As values they are compact and can easily be manipulated and transformed. For example, we present an explicit transformations between expansion tree proofs and cutfree sequential proofs. A theorem prover which represents proofs using expansion trees can use this transformation to present its proofs in more human-readable form. Also a very simple computation on expansion trees can transform them into Craig-style linear reasoning and into interpolants when they exist. We have chosen a sublogic of the Simple Theory of Types for our classical logic because it elegantly represents substitutions at all finite types through the use of the typed λ-calculus. Since all the proof-theoretic results we shall study depend heavily on properties of substitutions, using this logic has allowed us to strengthen and extend prior results: we are able to prove a strengthen form of the firstorder interpolation theorem as well as provide a correct description of Skolem functions and the Herbrand Universe. The latter are not straightforward generalization of their first-order definitions.

Table of Contents

§1. Introduction. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .1 §2. Logical Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2 §3. Expansion Tree Proofs. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .5 §4. Sequential Proofs. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .10 §5. Linear Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 §6. Skolemization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 Acknowledgements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 Bibliography . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

This paper appears in Studia Logica, Vol. 46, No. 4, 1987.