Home Philosophy Advances in ProofTheoretic Semantics


Explicit Composition and Its Application in Proofs of NormalizationAbstract The class of derivations in a system of logic has an inductive definition. One would thus expect that crucial properties of derivations, such as normalization in natural deduction or cut elimination in sequent calculus or consistency in arithmetic be proved by induction on the last rule applied. So far it has not been possible to implement this simple requirement uniformly. It is suggested that such proofs can be carried through by a 'Hilfssatz' methodology that is hidden in Gentzen's original unpublished proof of the consistency of arithmetic: to prove that a suitably chosen property of derivations is maintained under the composition of two derivations. As examples, new proofs by induction on the last rule in a derivation are given for normalization and strong normalization in natural deduction. IntroductionThe rules of inference of a logical system define an inductive class of formal derivations. The most natural way to prove properties for the class is by induction on the construction of derivations, i.e., by induction on the last rule applied. It is often a crucial component in such proofs to show that the property in question is maintained under the composition of two derivations, even if this aspect is regularly ignored and the composability of derivations taken for granted. Results that show composition to maintain properties of derivations were called Hilfssätze in work of Gentzen that remained unpublished in its time. His original proof of the consistency of arithmetic of 1935 contained a Hilfssatz by which the 'reducibility of sequents' is maintained under composition. After he changed this proof into one that used transfinite induction, all traces of the Hilfssatz disappeared (see von Plato 2015 [8] for details). A formal implementation of the Hilfssatz methodology requires that composition be made into an explicit rule that is added to the logical rules of a calculus. The following results are shown as illustrations of the use of such an explicit composition rule: (1) A proof of normalization by a Hilfssatz for intuitionistic natural deduction. (2) A proof of strong normalization by bar induction. Notation for Natural DerivationsThe rules of natural deduction are production rules by which the class of formal derivations is defined inductively. Whenever there is such a definition, the most natural way to prove properties of the corresponding class is by induction on the last rule applied. This is so also in proof theory; a proof of normalization for intuitionistic natural deduction is given as a first example. For a uniform treatment, we use natural deduction with general elimination rules and the related notion of normal derivability in which the condition is that the major premisses of elimination rules have to be assumptions. The modified rules are, with the multiplicity n, m ): 0 of closed formulas indicated by exponents as in An , Bm (Table 1). The normalizability result to be presented can be worked out also for the standard rules that can be seen as special cases of the general ones (Table 2). It will be convenient in this situation to leave out the degenerate derivations of the minor premisses, to have exactly the Gentzenian rules. In the standard tree notation for natural derivations, as above, the composition of two derivations can be indicated schematically, as in: Γ. . D and D.Δ . C compose into Γ. . D.Δ . C Ta ble 1 General E rules for & , ⊃, ∀ 1 1 1 1 An ,. Bm . A & B C & E ,1 C B.n . A ⊃ B A C C ⊃E ,1 A(t /. x )n . ∀xA C C ∀E ,1 Table 2 Gentzen's E rules as special cases of general E rules. 1 A & B A A & E ,1 1 A & B B B & E ,1 1 A ⊃ B A B B 1 ∀xA A (t /x ) ⊃E ,1 A(t /x ) ∀E ,1 Composition has the condition that the eigenvariables and discharge labels of the two derivations be distinct, if not, they can be changed. No trace is left of the composition in the rightmost derivation. As the calculus is defined by its logical rules, composition in natural deduction is usually left implicit. To represent the composition of two derivations formally and to reason about its properties in a convenient form, we write the logical rules and the additional rule of composition in sequent calculus style, with the open assumptions of each formula D in a derivation written out as a multiset Γ in a sequent Γ → D. More formally, we define a rootfirst translation into sequent calculus style. If the last rule is & I , we have: Γ. Δ. . . . . A B A & B & I '"V ∨I is similar, and ⊃I is: Γ → A Δ → B & I Γ, Δ → A & B 1 An.,Γ . n B A ⊃ B ⊃ I,1 '"V A ,Γ → B I Γ → A ⊃ B ⊃ The translation continues from the premisses until assumptions are reached. The logical rules of the calculus NLI are obtained by translating the rest of the logical rules into sequent notation. The nomenclature NLI was used in some early manuscripts of Gentzen to denote a “naturallogistic intuitionistic calculus” (Table 3). Table 3 Calculus NLI Γ → A & B An, Bm, Δ → C Γ , Δ → C &E Γ → A Δ → B &I Γ , Δ → A & B Γ → A ∨ B An, Δ → C Bm,Θ → C I1 Γ → B I2 Γ , Δ ,Θ → C ∨ Γ → A ∨ B ∨ Γ → A ∨ B ∨ Γ → A ⊃ B Δ → A Bm,Θ → C Γ , Δ ,Θ → C ⊃ Γ → ∀xA(x) A(t)n, Δ → C Γ , Δ → C Γ → ∃xA(x) A(y)n, Δ → C An,Γ → B Γ → A ⊃ B ⊃ Γ → A( y) Γ → ∀xA(x) ∀ Γ → A(t ) Γ , Δ C ∃E Γ xA(x) ∃I Natural deduction in sequent style The calculus is completed by adding initial sequents of the form A → A, with A an arbitrary formula, and the zeropremiss rule ⊥E by which ⊥ → C can begin a derivation branch. We say that the closing of an assumption formula in E rules and in rule ⊃I is vacuous if n = 0 or m = 0. Similarly, the closing of an assumption is multiple if n > 1 or m > 1. With n = 1 or m = 1, the closing of an assumption is simple. Vacuous and multiple closing of assumptions is seen in: 1 1 Γ. . B I A ⊃ B ⊃ A, A. ,Γ . B A ⊃ B ⊃ I,1 The former case corresponds to the situation in sequent calculus in which a formula active in a logical rule stems from a step of weakening, the latter to a situation in which it stems from a step of contraction, as shown in von Plato (2001) [5]. The composition of two derivations is an essential step in the normalization of derivations. It can now be written quite generally in the form: Γ → D D ,Δ → C Comp Γ, Δ → C Iterated compositions appear as so many successive instances of rule Comp. In a permutative conversion, the height of derivation of a major premiss derived by ∨E or ∃E , i.e., number of successive steps of inference, is diminished. The effect of the general rules is that such conversions work for all derived major premisses of elimination rules: Definition 1 A derivation in natural deduction with general elimination rules is normal if all major premisses of E rules are assumptions. As a first step towards normalization, we need to show that derivations in natural deduction can be composed: Lemma 1 (Closure of derivations with respect to composition) If given derivations of the sequents Γ → D and D,Δ → C in NLI are composed by rule Comp to conclude the sequent Γ, Δ → C, the instance of Comp can be eliminated. Proof We show by induction on the height of derivation of the right premiss of Comp that it can be eliminated. 1. Base case. The second premiss of Comp is an initial sequent, as in: Γ → D D → D Comp Γ → D The conclusion of Comp is identical to its first premiss, so that Comp can be deleted. If the second premiss is of the form ⊥ → D, the first premiss is Γ → ⊥. It has not been derived by a right rule, so that Comp can be permuted up in the first premiss. In the end, a topsequent Γ 1 → ⊥ is found as the left premiss of Comp, by which ⊥ is in Γ 1, so that the conclusion of Comp is an initial sequent. 2. Inductive case with the second premiss of Comp derived by an I rule. There are two subcases, a onepremiss rule and a twopremiss rule. In the former case, Comp is permuted up to the premiss, with a lesser height of derivation as a result. In the latter case, we use the notation (D) to indicate a possible occurrence of D in a premiss: (D), Δ1 → C1 (D), Δ11 → C11 Γ → D D, Δ1, Δ11 → C Comp Γ, Δ1, Δ11 → C Rule Rule Comp is permuted to any premiss that has an occurrence of D, say the first one, with the result: Γ → D D, Δ1 → C1 Comp Γ, Δ1 → C1 Γ, Δ1, Δ11 → C Δ11 → C11 Rule 3. Inductive case with the second premiss of Comp derived by an E rule, as in: (D), Δ → A & B (D), An , Bm ,Θ → C &E Γ → D D ,Δ,Θ → C Comp Γ, Δ, Θ → C As in case 2, Comp is permuted up, to whichever premiss has an occurrence of the composition formula D, with a lesser height of derivation as a result. The other cases of E rules are entirely similar. QED. In the case of a multiple discharge, a detour conversion will lead to several compositions, with a multiplication of the contexts as in the example Γ → A Δ → B &I Γ, Δ → A & B A , A , B ,Θ → C &E Γ, Δ, Θ → C The conversion is into Γ → A A , A , B ,Θ → C Comp Γ → A A , B ,Γ,Θ → C Comp Δ → B B ,Γ,Γ,Θ → C Comp Γ, Γ, Δ, Θ → C Such multiplication does not affect the normalization process. Note well that normalization depends on the admissibility of composition which latter has to be proved before normalization. 3 Normalization by Hilfssatz In normalization, derived major premisses of E rules are converted step by step into assumptions. There are two situations, depending on whether the major premiss was derived by an E rule or an I rule: Definition 2 (Normalizability) A derivation in NLI is normalizable if there is a sequence of conversions that transform it into normal form. The idea of our proof of the normalization theorem is to show by induction on the last rule applied in a derivation that logical rules maintain normalizability. The cut elimination theorem is often called Gentzen's Hauptsatz, main theorem. He used the word Hilfssatz, auxiliary theorem or lemma, for an analogous result by which composition of derivable sequents maintains the reducibility of sequents, a property defined in his original proof of the consistency of arithmetic (Gentzen 1935 [2, p. 106]). Henceforth any result in proof theory in which it is shown that a property of sequents or derivations is maintained under composition shall be called a Hilfssatz. Normalizability will be the first such property to be proved. Theorem 1 (Normalizability for intuitionistic natural deduction) Derivations in NLI convert to normal form. Proof Consider the last rule applied. The base case is an assumption that is a normal derivation. In the inductive case, if an I rule is applied to premisses the derivations of which are normalizable, the result is a normalizable derivation. The same holds if a normal instance of an E rule is applied. The remaining case it that a nonnormal instance of an E rule is applied. The major premiss of the rule is then derived either by another E rule or an I rule, so we have two main cases with subcases according to the specific rule in each. Derivations are so transformed that normalizability can be concluded either because the last rule instance resolves into possible nonnormalities with shorter conversion formulas, or because the height of derivation of its premisses is diminished. 1. E rules: Let the rule be &E followed by another instance of &E , as in: Γ → A & B An , Bm ,Δ → C & D Γ, Δ → C & D &E Γ, Δ, Θ → E Ck , Dl ,Θ E &E By the inductive hypothesis, the derivations of the premisses of the last rule are normalizable. The second instance of &E is permuted above the first: An , Bm ,Δ → C & D Ck , Dl ,Θ → E Γ → A & B An , Bm , Δ,Θ E &E &E Γ, Δ, Θ → E The height of derivation of the major premiss of the last rule instance in the upper derivation has diminished by 1, so the subderivation down to that rule instance is normalizable. The height of the major premiss of the other rule instance has remained intact and therefore normalizability follows. All other cases of permutative convertibility go through in the same way. 2. I rules: The second situation of convertibility is that the major premiss has been derived by an I rule, and there are five cases: 2.1. Detour convertibility on &: Γ → A Δ → B &I Γ, Δ → A & B An , Bm ,Θ C &E Γ, Δ, Θ → C Let us assume for the time being that n = m = 1. The detour conversion is given by: Γ → A A , B ,Θ → C Comp Δ → B B ,Γ,Θ → C Comp Γ, Δ, Θ → C The result is not a derivation in NLI . We proved in Lemma 1 that Comp is eliminable. The next step is to show that Comp maintains normalizability. This will be done in the Hilfssatz to be proved separately. By the Hilfssatz, the conclusion of the upper Comp is normalizable, and again by the Hilfssatz, also the conclusion of the lower Comp. If n > 1 or m > 1, Comp is applied repeatedly, the admissibility of an uppermost Comp giving the admissibility of the following ones. If n = 0, the instance of Comp with the left premiss Γ → A falls out of the derivation, and similarly with m = 0. If n = m = 0, the right premiss of rule & E before conversion is Θ → C, and it is taken in place of the original conclusion Γ, Δ, Θ → C. This situation is called a 'simplification convertibility' in Prawitz (1965) [3]. In all cases, the result of conversion is uniquely defined. 2.2. Detour convertibility on ∨. There are two cases, as in: Γ → A Γ → A ∨ B ∨I Am ,Δ → C Bn ,Θ → C Γ, Δ, Θ → C ∨E Γ → B Γ → A ∨ B ∨I Am ,Δ → C Bn ,Θ → C Γ, Δ, Θ → C ∨E As in 2.1, assume for the time being that n = m = 1. The detour conversion is given by: Γ → A A ,Δ → C Comp Γ → B B ,Θ → C Comp Γ, Δ → C Γ, Θ → C The multiplicities are treated as in 2.1, except for the case of m = 0 or n = 0. Then the given derivation has a simplification convertibility, say when m = n = 0: Γ → A Γ → A ∨ B ∨I Δ → C Θ → C Γ, Δ, Θ → C ∨E There is a conversion, but it is not uniquely defined: Either one of the original minor premisses of ∨E can be taken. Similarly, if say n > 0 and m = 0, either a composition with composition formula A can be made, or a simplification conversion. 2.3. Detour convertibility on ⊃I : An ,Γ → B Γ → A ⊃ B ⊃ Δ → A Bm ,Θ → C Γ, Δ, Θ → C ⊃E In the conversion, multiple discharge of assumptions is again resolved into iterated compositions, so we may assume n = m = 1 and have the conversion: Δ → A A ,Γ → B Comp Γ, Δ → B B ,Θ → C Comp Γ, Δ, Θ → C If m = 0, there is a simplification convertibility with the uniquely defined result Θ → C. 2.4. Detour convertibility on ∀: Γ → A ( y ) Γ → ∀x A(x ) ∀I An (t ), Δ → C Γ, Δ → C ∀E As before, assume for the time being that n = 1. The eigenvariable y in the derivation of Γ → A(y) is replaced by the term t and the detour conversion given by: Γ → A (t ) A (t ), Δ → C Comp Γ, Δ → C The multiplicities are treated as before. 2.5. Detour convertibility on ∃: Γ → A (t ) Γ → ∃x A(x ) ∃I An (y), Δ → C Γ, Δ → C ∃E As before, assume for the time being that n = 1. The eigenvariable y in the derivation of A(y), Δ → C is replaced by the term t , and the detour conversion is: Γ → A (t ) A (t ), Δ → C Comp Γ, Δ → C Multiplicities are treated as before. QED. It remains to give a proof of the Hilfssatz: Hilfssatz 1 (Closure of normalizability under composition) If the premisses of rule Comp are normalizable, also the conclusion is. Proof The proof is by induction on the length of the composition formula D with a subinduction on the sum of the heights of derivation of the two premisses. 1. D ≡ P. With an atomic formula P, we have Γ → P P ,Δ → C Comp Γ, Δ → C P is never principal in the right premiss, so that Comp can be permuted up with a lesser sum of heights of derivation as a result. There are two cases, a onepremiss rule and a twopremiss rule. For the latter, we use again the notation ( P) to indicate a possible occurrence of P in a premiss: ( P), Δ1 → C1 ( P), Δ11 → C11 Γ → P P, Δ1, Δ11 → C Comp Γ, Δ1, Δ11 → C Rule Rule Comp is permuted to the premiss that has an occurrence of P, say the first one, with the result: Γ → P P, Δ1 → C1 Comp P, Δ1 → C1 Γ, Δ1, Δ11 → C Δ11 → C11 Rule In the end, the second premiss of Comp is an initial sequent, as in: Γ → P P → P Comp Γ → P The conclusion of Comp is identical to its first premiss, so that Comp can be deleted. 2. D ≡ ⊥. Because ⊥ is never principal in the left premiss, Comp is permuted up as in the proof of admissibility of composition. 3. D ≡ A & B. If A & B is not principal in the right premiss, Comp can be permuted as in 1. If A & B is principal, there has to be a normal rule instance in the right premiss, as in: A & B A & B An , Bm ,Δ C &E Γ → A & B A & B ,Δ → C Comp Γ, Δ → C Comp is permuted up to the first premiss: Γ → A & B A & B → A & B Comp Γ → A & B An , Bm ,Δ C &E Γ, Δ → C Comp is now deleted and a generally nonnormal instance of rule &E created. If the major premiss is concluded by an E rule, a permutative conversion is done and no instance of Comp created. If the last rule is &I , a detour convertibility with the conversion formula A & B is created. A detour conversion will lead to new instances of Comp, but on strictly shorter formulas. The other cases of composition formulas are treated in a similar way. QED. Lemma 1, closure of derivations with respect to composition, merely shows that a derivation in natural deduction can be got from two composable derivations. The Hilfssatz adds the property of preservation of normalizability. It is even important to give the details for the composition of derivations as in the proof of Lemma 1, for the algorithm of normalization depends crucially on the steps needed for the admissibility of composition. Even so, one searches in vain for more than a mere indication of this proof in the logical literature. 
< Prev  CONTENTS  Next > 

Related topics 