e her derivation of Curry's paradox, we borrow Prawitz's system SN for the naive set theory introduced in Section 1.3 of Chapter 1. We use the following instances of ∈ −rules and have a natural deduction system SNC by adding the rule for classical reductio to SN . a ∈ a →⊥ ∈ I a ∈ {x|x ∈ x →⊥} a ∈ {x|x ∈ x →⊥} ∈ E a ∈ a →⊥ [¬φ]1 D ⊥ CR,1 φ Let R be a set of reduction procedures. A set R′ is an extension of R (R′ ⊇ R) if R′ results from R by adding reduction procedures which are closed under substitution in R′. Let S and S′ be any natural deduction system. S′ is an extension of S iff S′ is S itself or results from S by adding further rules. Then, SNC is an extension of SN . Also, we have a set RN of reduction procedures for ∧, →, and ¬. SNC has a set RNC by adding auxiliary reductions for CR−rule.1 While using CR−rule, auxiliary reduction procedures for the conclusion of CR−rule are added in the set of reductions. As Prawitz (1965, p. 34) does, the notion of a maximum formula is redefined as a major premise which is at the same time the conclusion of I− or CR−rules. A similar version of Rogerson's example is stated as below. Proposition 2.0.1. Let us define a parameter a as {x|x ∈ x →⊥}. Then, there is a closed derivation of ⊥ in SNC with respect to RNC which neither does generate a non-terminating reduction sequence nor is in normal form. Proof. Two claims show the result. Claim 1. There is a closed derivation Σ2 of ⊥ in SNC. 1Auxiliary reduction procedures for CR−rule will be introduced in Section 2.2. 32 First, there is an open derivation Σ1 of ⊥ from [¬a ∈ a]. [¬a ∈ a]1 [¬a ∈ a]1 [a ∈ a]2 ¬E⊥ → I,2a ∈ a →⊥ ∈ I a ∈ {x|x ∈ x →⊥} ************************ de f a ∈ a ¬E⊥ With the derivation Σ1, we have a closed derivation Σ2 as follows. [¬a ∈ a]1 Σ1 ⊥ CR,1a ∈ a ************************ de f a ∈ {x|x ∈ x →⊥} ∈ E a ∈ a →⊥ [¬a ∈ a]3 Σ1 ⊥ CR,3a ∈ a → E⊥ Claim