This post is largely a question about “a post on local reduction”:http://www.logicandlanguage.net/archives/2005/03/tonk_and_local_1.html on the new blog “logicandlanguage”:http://www.logicandlanguage.net/. Since it mostly reveals my ignorances, I’ll put it below the fold.

LL (our anonymous blogger) says that the usual propositional connectives have the following property:

bq. if anywhere in a proof there is an application of the introduction rule for a connective, followed immediately by an application of the elimination rule for that same connective _which takes the result of the introduction rule as its major premise, then the introduction and elimination pair can be eliminated_, leading to a more direct proof of the conclusion.

This is called the local reduction property. And I was wondering whether this is really true, or only on some formulations, or only in some logics? Because the following relatively well-known natural deduction proof looks like a counterexample to me. (I use ~T as a symbol for contradiction.)

1 (1) ~(p v ~p) A
2 (2) p A
2 (3) p v ~p 2, vI
1,2 (4) ~T 1,3, ~TI
1 (5) ~p 2,4 ~I
1 (6) p v ~p 5, vI
1 (7) ~T 1,6 ~TI
   (8) ~~(p v ~p) 1, 7, ~I
   (9) p v ~p 8, ~E

It looks to me like at (8) I used a connective’s intro rule, and at (9) used the very same connective’s elim rule, with (8) as the main (indeed only) premise, but I can’t eliminate those two steps from the proof. Am I missing something here?

I could be missing the fact that ~E is not really a logical rule. (Some days I think the acceptability of ~E is synthetic a priori, which isn’t possible if it is a logical rule.) Then all the connectives might have the local reduction property. Or I could be working in the wrong proof theory. But this looks like a counterexample to the claim that all of the familiar connectives have the local reduction property.