l proofs, and affording a solution to the problem of overgeneration. The fourth reason is related to our topic. Fourth, ... using Elimination rules in [generalized] form affords a solution to certain problems that would otherwise arise for the proof-theoretic criterion of paradoxicality ... . (Tennant, 2017, p. 110) When Tennant (2016) and Tennant (2017, Ch. 11) deal with the problem of overgeneration occurred by Ekman's paradox, instead of accusing Ekman reduction ⊵E of the problem, he provides a solution that all elimination rules are stated in generalized form.10 Though he believes that the choice of the form of generalized elimination rules can solve the overgeneration problem, it also provides a case that causes the undergeneration problem. We now consider the second case that raises the problem of undergeneration without classical inferences. When we use generalized form of elimination rules with permutation conversions, there is a closed full normal derivation of ⊥ which formalizes the Liar paradox. For the example, we have the generalized elimination rules for the truth-predicate T (x) and its standard reduction process. D1 φ T I T (⌜φ⌝) T (⌜φ⌝) [φ]1 D2 ψ T E,1 ψ 9With respect to the problem of overgeneration, the issue with tests of a proper reduction will be discussed in Chapter 3. 10The assessment of his solution will be discussed in the next chapter. 54 The reduction procedure for T (x) D1 φ T I T (⌜φ⌝) [φ]1 D2 ψ T E,1 ψ ▷T (x) D1 φ D2 ψ Also, we take = E−rule having the form of the generalized elimination rule. t1 = t2 D1 φ(t1) [φ(t2)] 1 D2 ψ = E,1 ψ Then, Proposition 2.3.1 shows that there exists a full normal derivation of ⊥ from the Liar paradox. Proposition 2.3.1. Let SR be a system containing T−, ¬−, =−rules with their generalized form of elimination rules. SR has a set RR of reduction procedures for T (x) and ¬, and ⊵Sub with permutation conversion. Suppose that, for some formula Φ, ⌜Φ⌝= ⌜¬T (⌜Φ⌝)⌝ is an axiom of SR. There exists 