n D1 of ⊥ from [φ →¬φ] and [φ]. [φ →¬φ]1 [φ]2 → E¬φ [φ]2 ¬E⊥ 93 With the derivation D1, we have an open derivation D2 of φ from [φ →¬φ] and [¬φ → φ]. [¬φ → φ]3 [φ →¬φ]1, [φ]2 D1 ⊥ ¬I,2¬φ ¬E φ Now, we have the following open derivation Π1 of ⊥ from [φ →¬φ] and [¬φ → φ]. [φ →¬φ]1, [φ]2 D1 ⊥ ¬I,2¬φ [φ →¬φ]1, [¬φ → φ]3 D2 φ ¬E⊥ Claim 2. If an Ekman reduction process is used for Π1, then Π1 generates a non-terminating reduction sequence and is not normalizable. Π1 has a maximum formula ¬φ in ¬E−rule. By applying ¬−reduction, we have the following derivation Π2. [φ →¬φ]1 [¬φ → φ]3 [φ →¬φ]1, [φ]2 D1 ⊥ ¬I,2¬φ → E φ → E¬φ [φ →¬φ]1, [¬φ → φ]3 D2 φ ¬E⊥ The derivation Π2 has no maximum formula but it has an Ekman maximum formula. By applying Ekman reduction, we obtain the same derivation with Π1 which we started. Therefore, if the set of reductions of SE includes Ekman reduction, Π1 initiates a non-terminating reduction sequence and so is not normalizable. 94 We call the result of Proposition 3.1.1 Ekman's paradox. Schroeder-Heister and Tranchini (2017, pp. 570-571) appear to think that the derivation Π1 uses id est inference since Π1 has inferences from φ to ¬φ and ¬φ to φ . Also, Π1 is a derivation of ⊥ and generates a reduction loop. Hence, according to TCPE , Π1 is a T-paradox. Thus, Ekman's paradox can be a counterexample to TCPE . Schroeder-Heister and Tranchini (2017, p. 571) diagnose the phenomenon, by saying, ... we take Ekman's paradox to push the question of when a certain reduction counts as acceptable: whether a derivation is normal depends on the collection of reductions adopted, and hence Tennant's criterion requires particular attention in what should be taken to be a good reduction. In particular, Ekman's phenomenon shows that on a too loose notion of reduction, one obtains a too coarse criterion of paradoxicality. According to their diagnosis, the occu