Strong Normalization by Bar Induction

Derivations are denoted by d0, d1, d2,... , and let N (d) express that d is a normal derivation, i.e., that all major premisses of E -rules are initial sequents. This property can be decided by an inspection of the derivation. The choice sequences in normalization are defined as follows:

Definition 3 (Conversion choice sequence for a derivation) Given a derivation d, a conversion choice sequence for d is a succession of conversions on d with the restriction that whenever d has a permutative convertibility, it has to be chosen.

The restriction is in fact not necessary, but it will make the proof go through smoothly. It is not met if disjunction and existence are left out of the language and the standard elimination rules used, so there is sense in calling the result of this Section a strong normalization theorem.

We shall indicate by PF(d) that a derivation d is free of permutative conversions. The notation αn (d)dn stands for the derivation that is obtained from a given derivation d after n steps of conversion αn . The notation α1(αn (d))α1 (dn ) stands

for the result of a one-step continuation of the sequence of conversions αn .

Definition 4 (Normalizing and strongly normalizing derivations)

i. A derivation d is normalizing whenever ∃αxN (αx (d)).

ii. A derivation d is strongly normalizing whenever ∀αxN (αx (d)).

We write WN(d) for the former and SN(d) for the latter.

We shall use the standard formulation of bar induction in the proof of strong normalization, with the two predicates PF(d) and SN(d). It has to be established that:

(1) The base case predicate PF(d) is decidable. (2) Every conversion choice sequence of a given derivation d has an initial segment such that a permutation-free derivation is obtained. (3) Permutation-free derivations are strongly normalizing. (4) If every one-step continuation of conversions of a derivation d is strongly normalizing, also d is strongly normalizing.

Theorem 2 (Strong normalization for intuitionistic natural deduction) Derivations in NLI are strongly normalizing.

Proof We show in turn that the four conditions of bar induction are satisfied by the predicates PF(d) and SN(d). Let d0 be the given derivation that we assume to be non-normal.

1. Decidability: PF(d) is decidable as noted above.

2. Termination of permutative conversions: Let a derivation d have permutative convertibilities. As seen in the proof of normalization, each such conversion diminishes the height of derivation of the major premiss in question by 1 and leaves the other heights unaltered. Therefore permutative conversions terminate in a bounded number n of steps in a derivation dn such that PF(dn ).

3. If PF(d), then SN(d): The proof is by induction on the last rule in d and we can assume d not to be normal and the derivations of the premisses to be strongly normalizing. By PF(d), all non-normalities are detour convertibilities. Any conversion chosen resolves into compositions, and a Hilfssatz needs to be proved by which composition of derivations maintains strong normalizability. This is done below.

4. Ifα1SN (α1(dn )), then SN(dn ): Each one-step continuation of the conversion

of dn is by assumption strongly normalizing, therefore the derivation dn is by

definition strongly normalizing.

By 1–4, SN(d0). QED.

It remains to add a proof of the Hilfssatz used in condition 3:

Hilfssatz 2 (Closure of strong normalizability under composition) Given strongly normalizing derivations of Γ D and D,Δ C, their composition into a derivation of Γ, Δ C is strongly normalizing.

Proof As before, the proof is by induction on the length of the composition formula D, with a subinduction on the sum of heights of derivation of the premisses of rule Comp, and goes through virtually identically to the proof of Hilfssatz 1. QED.

< Prev   CONTENTS   Next >