lative to R except D1 itself. Definition 1.2.5. A derivation D is normal (or in normal form) relative to R iff D is irreducible relative to R, i.e. D has no maximum formula. A reduction sequence terminates iff it has a finite number of derivations and its last derivation is in normal form. A derivation D is normalizable relative to R iff there is a terminating reduction sequence relative to R starting from D. D is strongly normalizable relative to R iff every reduction sequence relative to R that starts from D terminates.7 Definition 1.2.6. A reduction procedure φ1, ...,φn D ψ ▷ φ1, ...,φn D′ ψ in R is closure under substitution iff, for any derivation D1 φ1 , ..., Dn φn , a reduction procedure D1 φ1 , ..., Dn φn D ψ ▷ D1 φ1 , ..., Dn φn D′ ψ is in R as well. Prawitz (1965, 1971) has proved (weak) normalization theorem for the first order intuitionistic logic which says that each derivation in a system for the first order intuitionistic 6For any term x and y, let x ⩽ y mean that x is less than or equal to y. 7When all elimination rules are stated in generalized form, the set R of reduction procedures has additional reduction procedures, called permutation conversion. Then, an irreducible derivation is the same as the derivation that all major premises are assumptions or not derived by any rules in a given system. In that case, we shall use 'full normal form' and 'full normalizable' rather than 'normal form' and 'normalizable.' Generalized elimination rules and related terminologies will be introduced in Chapter 2. In addition, if there is no misunderstanding, for our convenience sake, we drop the 'relative to R in the suggested notions. 22 logic reduces to be in normal form. The corollary of the result is that every (closed) derivation in the system can be reduced to one using an introduction rule in the last step. Since no introduction rule derive an absurdity (⊥) as its conclusion, normalization theorem implies that there is no derivation of ⊥ in the system, i.e. the consistency of t