reiteration rule shouldn't be basic

[jonathanichikawa]

The "Reiteration" natural deduction rule is listed as a basic, not a derived, rule. This is unnecessary — it can be derived via or-introduction, negation elimination, and negation elimination. Need to add a discussion of the fact to the derived rules section, and move the R rule from the basic page to the derived page in the appendix.

[jonathanichikawa]

I think I was mistaken about this. Given the way our reductio rules are written, I don't think we can derive R from the introduction and elimination rules after all. I had been thinking along these lines:

But this is a mistake; line 4 would have needed to reference the double negation, which is not what we have on 1.

So unless/until I figure out how to derive R, I'll leave it as basic.

[Nico314159]

You can derive R as follows:

1. φ
2. φ ∧ φ (∧I, 1, 1)
3. φ (∧E, 2)

[jonathanichikawa]

I made this change.