The rule of repetition, implicit or explicit?

---

In most formulations of Natural Deduction, it is assumed that (1) the same formula may be repeated in the process of proof, and that (2) the same formula may be used twice, once as an assumption and then as a consequence from it. Thus, for instance, in my (linear) formulation (see Uchii 1989, 40 ff.), it may be all right to write as follows:

1. A 　　[assumption]

2. A 　　[1, repetition]

3. A⊃A 　[1,2, ⊃-intro];

or more briefly,

1. A 　　[assumption]

2. A⊃A 　[1, ⊃-intro] .

But, since according to the "spirit" of logic everything should be made explicit, it seems desirable to state the rule of repetition:

A / A 　(you may repeat the same formula, as a consequence)

Although this may seem trivial, it must be noticed that "A⊃A" cannot be proved easily in the intuitionistic system (which does not have the elimination of double negation) without this rule (although the proof is possible, as some student has shown). Thus, it is better to state this rule, and then to show that this rule can be derived from other primitive rules.

In conclusion, although the rule of repetition looks desirable from the pedagogical point of view, it can be shown to be obtainable as a derived rule (proof is by no means trivial in the intuitionistic system).

　

Uchii, S. (1989) 『真理・証明・計算』ミネルヴァ書房、1989。