duction system. Let SEG be a natural deduction system containing ∧I−, → I−, ¬I−rules with the generalized form of elimination rules. Plus, we define φ ↔ ¬φ as (φ → ¬φ)∧ (¬φ → φ). Proposition 3.2.1 is the answer of Tennant (2016, 2017) against Ekman's paradox. His solution says that a non-terminating reduction sequence does not arise if one insists on the application of the generalized form of elimination rules. Proposition 3.2.1. There is an open full normal derivation of ⊥ from [φ →¬φ] and [¬φ → φ] in SEG. Proof. The result consists of two claims. Claim 1. There is an open derivation D3 of ⊥ from φ →¬φ and ¬φ → φ . First, there is an open derivation D1 of ⊥ from [φ →¬φ] and [φ]. [φ →¬φ]4 [φ]2 [¬φ]1 [φ]2 [⊥]3 → E,3⊥ → E,1⊥ 96 Then, we have an open derivation D2 of φ from [φ →¬φ] and [¬φ → φ]. [¬φ → φ]4 [φ]2, [φ →¬φ]4 D1 ⊥ ¬I,2¬φ [φ]5 → E,5 φ Now, we have an open derivation D3 of ⊥ from [φ →¬φ] and [¬φ → φ]. [φ →¬φ]4 [¬φ → φ]4 [φ]2, [φ →¬φ]4 D1 ⊥ ¬I,2¬φ [φ]5 → E,5 φ [¬φ]7 [φ →¬φ]4, [¬φ → φ]4 D2 φ [⊥]6 ¬E,6⊥ → E,7⊥ Claim 2. D3 is in full normal form. Since all major premises in D3 are assumptions, D3 is in full normal form. Ekman reduction process is stated in the form of standard elimination rules. We cannot apply it to D3, and thus D3 is in full normal form. D3 does not satisfy TCPE and so is not a T-paradox. Furthermore, we readily have the following result from the derivation D3 of Proposition 3.2.1. Proposition 3.2.2. There is a closed full normal derivation D4 of ¬(φ ↔¬φ) in SEG. Proof. Two claims verify the result. Claim 1. there is a closed derivation D4 of ¬(φ ↔¬φ). From the proof of Proposition 3.2.1, SEG has an open derivation D3 of ⊥ from [φ →¬φ] 97 and [¬φ → φ]. Then, we have a closed derivation D4 of ¬(φ ↔¬φ). [(φ →¬φ)∧ (¬φ → φ)]8 [φ →¬φ]4, [¬φ → φ]4 D3 ⊥ ∧E,4⊥ ¬I,8¬((φ →¬