's paradox which generates a non-terminating reduction sequence. The use of axioms may cause to prevent the occurrence of a non-terminating reduction sequence. That is to say, an application of an axiom, which can lead to a formula that has a principal constant but has no reduction process to remove the formula, can disguise a non-terminating reduction sequence. Similar to the case of Curry's paradox, Tennant-style derivation ∆3 of the Liar paradox in Proposition 2.2.1 can produce a looping reduction without ⊵Sub−reduction when there is a standard reduction process to eliminate the formula ⌜¬T (⌜Φ⌝)⌝= ⌜Φ⌝. Let us consider the following rules for an equation between coded numerals.14 [φ]1 D1 ψ [ψ]2 D2 φ ⌜⌝I,1,2⌜φ⌝= ⌜ψ⌝ ⌜φ⌝= ⌜ψ⌝ D3 φ ⌜⌝E1 ψ ⌜φ⌝= ⌜ψ⌝ D4 ψ ⌜⌝E2 φ 14⌜⌝E−rules are what Tennant (1982, p. 289) calls 'Leibniz disquatational rule.' 72 Standard reductions for ⌜⌝−rules are described as below. [φ]1 D1 ψ [ψ]2 D2 φ ⌜⌝I,1,2⌜φ⌝= ⌜ψ⌝ D3 φ ⌜⌝E1 ψ ▷⌜⌝1 D3 φ D1 ψ [φ]1 D1 ψ [ψ]2 D2 φ ⌜⌝I,1,2⌜φ⌝= ⌜ψ⌝ D4 ψ ⌜⌝E2 φ ▷⌜⌝2 D4 ψ D2 φ When we presume that a liar sentence Φ which is defined by ¬T (⌜Φ⌝) is expressible in our language, there is a derivation of the Liar paradox using the formula ⌜¬T (⌜Φ⌝)⌝ = ⌜Φ⌝ which raises a non-terminating reduction sequence. Proposition 2.4.4. Let SL be a system containing T−, ¬−, and ⌜⌝−rules. SL has a set RL of standard reduction procedures for T (x), ¬, and ⌜⌝. Let us define a formula Φ as ¬T (⌜Φ⌝). Then, there exists a closed derivation Π11 of ⊥ in SL with respect to RL which generates a non-terminating reduction sequence, and so is not normalizable. Proof. Two claims establish the result. Claim 1. There is a closed derivation Π11 of ⊥ in SL with respect to RL. First, there is an open derivation Π9 of ⊥ from T (⌜Φ⌝). [Φ]1 ************* de f ¬T (⌜Φ⌝) [¬T (⌜Φ⌝)]2 *************