# Strong Normalization by Bar Induction

Derivations are denoted by *d*0*, d*1*, d*2*,...* , 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 i__s____ __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 *d*0 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* ∀*α*1*SN (α*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(d*0*)*. 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.