awitz (1965) firstly investigates that a derivation of an absurdity from the set-theoretic paradox falls into a non-terminating reduction sequence. Though he did not explicitly mention that the non-terminating reduction sequence is the distinguishing feature of the paradoxes, it is often said that he would do so. For instance, Schroeder-Heister and Tranchini (2017, p. 568) said, 'Prawitz proposed [the non-terminating reduction sequence] to be the distinguished feature of Russell's paradox.' Further to Prawitz, Tennant (1982) suggests the proof-theoretic criterion for paradoxicality and it has been developed by Tennant (1995, 2016, 2017). Let us take the natural deduction system SN for the naive set theory in the same manner of Prawitz (1965, Appendix B) which only contains the rules for ∧, →, ¬, and the following additional rules: D φ[t/x] ∈ I t ∈ {x|φ(x)} t ∈ {x|φ(x)} ∈ E φ[t/x] ∈ −rules have the following standard reduction process. D φ[t/x] ∈ I t ∈ {x|φ(x)} ∈ E φ[t/x] ▷∈ D φ[t/x] Let us define a parameter a as {x|¬x ∈ x}. Then, an application of ∈ I−rule to ¬a ∈ a derives a ∈ a and an application of ∈ E−rule to a ∈ a derives ¬a ∈ a. Prawitz (1965, p. 95) investigates that a derivation of ⊥ from Russell's paradox cannot be transformed into a 24 normal derivation because it raises an infinite reduction sequence. Proposition 1.3.1. Let us define a parameter a as {x|¬x ∈ x}. Then, there is a closed derivation of ⊥ in SN which generates a non-terminating reduction sequence and so is not normalizable. Proof. Two claims justify the result. Claim 1. there exists a closed derivation D3 of ⊥. First, there is an open derivation D1 of ⊥ from [a ∈ a]. [a ∈ a]1 ******************** de f a ∈ {x|¬x ∈ x} ∈ E¬a ∈ a [a ∈ a]1 ¬E⊥ With the derivation D1, we have a closed derivation D2 of a ∈ a. [a ∈ a]1 D1 ⊥ ¬I,1¬a ∈ a ∈ I a ∈ {x|¬x ∈ x} ******************** de f a ∈ a Then, we have a closed derivation D3 of ⊥. [a ∈ a]1 D1 