Wednesday, November 11, 2009

Independence of Reductio

The other day I was wondering whether one can have a complete propositional calculus with only the introduction and elimination rules for each connective. So you have modus ponens and conditional proof, but not modus tollens and contraposition; or-introduction and or-elimination, but not disjunctive syllogism; &-intro and &-elim, but not "modus ponendo tollens", i.e. from ~(A & B) and A to infer ~B. In particular, you don't have reductio ad absurdum, from A & ~A to infer B.

Such a system seems simple and intuitive, but I don't see how to do it. At a minimum, we should be able to prove p & ~p -> q from the introduction and elimination rules alone, but I haven't been able to prove it. You can get it assuming any of the principles we've ruled out, e.g. modus tollens, contraposition, or disjunctive syllogism. For example (using / as a turnstile):

1. {p & ~p} / p & ~p (Assumption)
2. {p & ~p} / p (&-elim, 1)
3. {p & ~p} / ~p (&-elim, 1)
4. {~q} / ~q (Assumption)
5. {p & ~p, ~q} / p & ~q (&-intro, 2, 4)
6. {p & ~p, ~q} / p (&-elim, 5)
7. {p & ~p} / ~q -> p (->-intro, 6)
8. {p & ~p} / ~~q (MODUS TOLLENS, 3, 7)
9. {p & ~p} / q (~-elim, 8)
10. / (p & ~p) -> q (->-intro, 9)

The proof assuming contraposition is similar, but instead we show ~p -> ~q (using ~p where we have p in lines 5-7), contrapose, and use p and ->-elim to conclude q (rather than ~p and modus tollens). For disjunctive syllogism, the proof is even simpler:

1. {p & ~p} / p & ~p (Assumption)
2. {p & ~p} / p (&-elim, 1)
3. {p & ~p} / p v q (v-intro, 2)
4. {p & ~p} / ~p (&-elim, 1)
5. {p & ~p} / q (DISJUNCTIVE SYLLOGISM, 3, 4)
6. / (p & ~p) -> q (->-intro, 5)

What's more, we can prove any of these rules (modus tollens, contraposition, disjunctive syllogism) by assuming reductio (it's an easy exercise). So it follows that if we can prove any of these four rules from Assumption and the intro and elimination rules, our system is complete (well, it doesn't follow per se, but I could show you, if asked).

So, here's what I want to know from my readers, few though they may be. Can you prove reductio, modus tollens, contraposition, or disjunctive syllogism from just the intro and elimination rules? And if not, why not? Why does a complete propositional calculus need something other than the intro and elimination rules? I feel like this is something I should've learned in logic, but never did.

(Aside: yes, I know this post is going to make me look foolish when someone presents the answer, whatever it is. So be it.)