 the degree of a maximum formula and satisfies the inversion principle whereas the auxiliary reduction procedures are often proposed independently of the inversion principle. For example, ⊵Sub−reduction above is just lowering the length of a derivation and its role does not seem to pursue the inversion principle. Also, the following reductions are different from the standard reductions. 3. The auxiliary reduction procedure for CR−rule with regard to ¬−rules. [¬¬φ]1 D ⊥ CR,1¬φ ⊵CR(¬) [¬⊥]3 [¬φ]1 [φ]2 ¬E⊥ ¬E⊥ ¬I,1¬¬φ D ⊥ CR,3⊥ ¬I,2¬φ 4. The auxiliary reduction procedure for CR−rule with regard to T−rules. [¬T (⌜φ⌝)]1 D ⊥ CR,1T (⌜φ⌝) ⊵CR(T (x)) [¬φ]2 [T (⌜φ⌝)]1 T E φ ¬E⊥ ¬I,1¬T (⌜φ⌝) D ⊥ CR,2 φ T I T (⌜φ⌝) ⊵CR(¬)− and ⊵CR(T (x))−reductions neither do eliminate a maximum formula nor lower the length of a derivation, but they lower the degree of the conclusion of CR−rule. Tennant (2015, pp. 585–588) proposes a derivation of the Liar paradox which does not employ CR−rule and does generate a looping reduction sequence. We will use a natural 47 deduction system SE which has ¬−, T−, =−rules. A set RE of reductions contains ▷¬−, ▷T (x)−, and ⊵Sub. Then, we have the result in SE with respect to RE . Proposition 2.2.1. Suppose that, for some formula Φ, ⌜Φ⌝ = ⌜¬T (⌜Φ⌝)⌝ is an axiom of SE . SE relative to RE has a closed derivation of ⊥ which generates a non-terminating reduction sequence, so is not normalizable. Proof. The result consists of two claims Claim 1. there is a closed derivation ∆3 of ⊥ in SE We begin with an open derivation ∆1 of ⊥ from [T (⌜Φ⌝)]. Ax1⌜Φ⌝= ⌜¬T (⌜Φ⌝)⌝ [T (⌜Φ⌝)]1 = E T (⌜¬T (⌜Φ⌝)⌝) T E¬T (⌜Φ⌝) [T (⌜Φ⌝)]1 ¬E⊥ With the open derivation ∆1, we have the closed derivation ∆2 of T (⌜φ⌝). Ax2⌜¬T (⌜Φ⌝)⌝= ⌜Φ⌝ [T (⌜Φ⌝)]1 ∆1 ⊥ ¬I,1¬T (⌜Φ⌝) T I T (⌜¬T (⌜Φ⌝)⌝) = E T (⌜Φ�