la derived by any rules. So, the derivation ∆8 of ⊥ in Proposition 2.3.1 is in (full) normal form and does not generate a non-terminating reduction sequence. We can have a similar case of Curry's paradox by using a formula, ¬a ∈ a ↔ a ∈ {x|x ∈ x → ⊥} as an axiom. 56 As we have seen at the beginning of this chapter, the formalization of Curry's paradox needs to use ∈ −rules. Let us consider a derivation of Curry's paradox which does not employ ∈−rule. Our natural deduction system has introduction and (standard) elimination rules for ∧, →, and ¬. We define a parameter a as a set {x|x ∈ x →⊥} and instead of using ∈−rules we regard (a ∈ a →⊥)↔ a ∈ {x|x ∈ x →⊥} as an axiom of our system. For our convenience sake, we use the following abbreviations: D a ∈ a →⊥ SetI a ∈ {x|x ∈ x →⊥} is an abbreviation for Ax (a ∈ a →⊥)↔ a ∈ {x|x ∈ x →⊥} ********************************************************************************************** de f ((a ∈ a →⊥)→ a ∈ {x|x ∈ x →⊥})∧ (a ∈ {x|x ∈ x →⊥}→ (a ∈ a →⊥)) ∧E (a ∈ a →⊥)→ a ∈ {x|x ∈ x →⊥} D a ∈ a →⊥ → E a ∈ {x|x ∈ x →⊥} Also, D a ∈ {x|x ∈ x →⊥} SetE a ∈ a →⊥ is an abbreviation for Ax (a ∈ a →⊥)↔ a ∈ {x|x ∈ x →⊥} ********************************************************************************************** de f ((a ∈ a →⊥)→ a ∈ {x|x ∈ x →⊥})∧ (a ∈ {x|x ∈ x →⊥}→ (a ∈ a →⊥)) ∧E a ∈ {x|x ∈ x →⊥}→ (a ∈ a →⊥) D a ∈ {x|x ∈ x →⊥} → E a ∈ a →⊥ 57 Then, there is an open derivation ∆9 of ⊥ from [a ∈ a] [a ∈ a]1 ************************ de f a ∈ {x|x ∈ x →⊥} SetE a ∈ a →⊥ [a ∈ a]1 → E⊥ With the derivation ∆9, we have a closed derivation ∆10 of a ∈ a. [a ∈ a]1 ∆9 ⊥ → I,1a ∈ a →⊥ SetI a ∈ {x|x ∈ x →⊥} ************************ de f a ∈ a Now, we have a closed derivation ∆11 of ⊥. [a ∈ 