paradox proposed in Tennant (2015, pp. 585–590).12 Let SCRE be a natural deduction system containing ¬−, T−, =−, CR−, and CRE−rules which is an extension of SCE used in Section 2.2. We have a set RCRE of standard reduction procedures having ▷¬, ▷T (x), ▷=, ▷CRE , and the following auxiliary reduction ⊵T (x). D T (⌜φ⌝) T E φ T I T (⌜φ⌝) ⊵T (x) D T (⌜φ⌝) Then, we have the following result. Proposition 2.4.3. Suppose that, for some formula Φ, ⌜Φ⌝ = ⌜¬T (⌜Φ⌝)⌝ is an axiom of 12While Tennant (2016, pp. 12–16) claims that the Liar paradox is a genuine paradox, he employs the id est rules for the liar sentence Ψ. By using his id est rules and a derivation of the Liar paradox, we have similar results. Appendix 2.A shows that there are three closed derivations of ⊥ which formalize the Liar paradox: (i) a T-paradox which use neither CR− nor CRE−rules, (ii) a T-paradox using both CR−and CRE−rules, and (iii) a derivation of ⊥ which only uses CR−rule and is not a T-paradox. 68 SCRE . SCRE relative to RCRE has a closed derivation of ⊥ which initiates a non-terminating reduction sequence, so is not normalizable. Proof. Two claims verify the result. Claim 1. There is a closed derivation Π7 of ⊥ in SCRE . We start with an open derivation Π5 of ⊥ from [¬T (⌜Φ⌝)]. Ax2⌜¬T (⌜Φ⌝)⌝= ⌜Φ⌝ [¬T (⌜Φ⌝)]1 T I T (⌜¬T (⌜Φ⌝)⌝) = E T (⌜Φ⌝) [¬T (⌜Φ⌝)]1 CRE⊥ With the derivation Π5, we have a closed derivation Π6 of ¬T (⌜Φ⌝). Ax1⌜Φ⌝= ⌜¬T (⌜Φ⌝)⌝ [¬T (⌜Φ⌝)]2 Π5 ⊥ CR,2T (⌜Φ⌝) = E T (⌜¬T (⌜Φ⌝)⌝) T E¬T (⌜Φ⌝) Then, we have a closed derivation Π7 of ⊥. [¬T (⌜Φ⌝)]1 Π5 ⊥ CR,1T (⌜Φ⌝) Π6 ¬T (⌜Φ⌝) CRE⊥ Claim 2. Π7 initiate a non-terminating reduction sequence, and so is not normalizable. Since Π7 has a maximum formula T (⌜Φ⌝) in the last CRE−rule, by applying ▷CRE to 69 Π7, we have a derivation Π8 below. Ax2⌜¬T (⌜Φ⌝)⌝= ⌜Φ⌝ Ax