ination rules for ◦ are intrinsically harmonious iff every pair consisting of an ◦I− and ◦E−rules satisfies the inversion principle. Not all pairs of introduction and elimination rules satisfy intrinsic harmony. Intrinsic harmony requirement should demand that every pair of introduction and elimination rules satisfy the inversion principle. Let us consider a well-known example of tonk−rules introduced by Arthur Prior (1960) with some variation. Di φi tonkIi(i = 1,2) φ1 tonk φ2 φ1 tonk φ2 tonkEi(i = 1,2) φi tonkI−rules have the same form of ∨I−rules, but tonkE−rules have the standard form of ∧E−rules. tonk−rules derive any formulas and are problematic. For instance, D1 φ1 tonkI1 φ1 tonk φ2 tonkE2 φ2 From the derivation D1 of φ1, tonkI1− and tonkE2−rules can have any consequences. If the intrinsic harmony requirement only demands a pair of introduction and elimination rules satisfying the inversion principle, tonk−rules have a reduction process between tonkI1− and tonkE1−rules and are not problematic. 41 D1 φ1 tonkI1 φ1 tonk φ2 tonkE1 φ1 ▷ D1 φ1 However, no reduction procedure exists between tonkI1− and tonkE2−rules (also between tonkI2− and tonkE1−rules). Therefore, in order to block tonk−rules, we will request any pair of introduction and elimination rules satisfies the inversion principle. Dummett (1991, p. 287) considers that intrinsic harmony may be too weak requirement. Roughly, intrinsic harmony prevents elimination rules to be stronger than the corresponding introduction rules whereas it does not restrict elimination rules which is weaker than the corresponding introduction rules. For example, we consider the following form of rules for ▲. D1 φ D2 ψ ▲I φ▲ψ φ▲ψ ▲E φ ▲−rules are intrinsically harmonious, but yet ▲E−rule does not fully infer any consequences of the meaning of φ▲ψ conferred by ▲I−rule. So to speak, elimination rules should be neither stronger nor weaker than the corresponding introduction rules. For