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.)
Subscribe to:
Post Comments (Atom)
Hi Michael,
ReplyDeleteThe question is: which negation rules do you want to use? With the elim/intro rules for conjunction and implication, you won't even get the positive fragment of classical logic (since Peirce's Law isn't provable). However, if you add classical reductio (assume ¬A, if you can derive a contradiction, conclude A and discharge ¬A), you get full classical logic. The problem is that it's difficult to place the rule neatly in either the intro or the elim category. On the other hand, if you add EFQ (from a contradiction, conclude B for arbitrary B), you get full intuitionistic logic. These are basically the systems from Prawitz 1965.
Of course, these rules involve absurdity as a primitive in the language. If you want straight negation rules, the usual intro/elim pair is intuitionistic reductio (assume A, if you can derive a contradiction, conclude ¬A and discharge A) as the intro-rule for negeation, and the elim rule is an EFQ version (from A, ¬A conclude B). That's not enough for classical logic, but adding double negation elimination is.
There is a variety of other intro and elim rules for negation, most of them motivated by different ways of getting proof-theoretic properties like normalisation, subformula property, etc. The general problem is that classical logic (in single conclusion framework) lack negation rules which are as "nice" as intuitionistic logic. (Although I don't think anything philosophically interesting follows from that.)
Ole,
ReplyDeleteThanks for the reply. I guess I had assumed the intro and elimination rules for negation were:
p / ~~p (~-intro)
~~p / p (~-elim)
But you're right, that won't help. Since intro and elim for ->, v, and & won't get us a complete logic, it's not clear why adding the above two rules would help.
I guess my worry was, as you say, that other rules one can add don't seem like either intro or elimination for negation.
But I am confused by your distinction between classical reductio and intuitiionistic reductio. Your classical reductio is:
From: G, A / B & ~B
To: G / ~A
And your intuistionist reductio (EFQ) is:
From: G / B & ~B
To: G / A
And you suggest adding the former as ~-intro and the latter as ~-elim. But you can derive the latter from the former:
1. G / B & ~B (by supposition)
2. ~A / ~A (by assumption)
3. G, ~A / ~A & (B & ~B) (&-intro, 1, 2)
4. G, ~A / B & ~B (&-elim, 3)
5. G / ~~A (classical reductio, 4)
6. G / A (double negation, 5)
The derivation doesn't work without double negation, but once you have that, there's no reason for both rules, yes?
But thanks, I think I'm generally clearer on these issues now. I should read up on intuitionistic logic.
Hi,
ReplyDeleteYes, you won't get classical logic by just including the intro and elim rules
p / ~~p (~-intro)
~~p / p (~-elim)
The crucial difference is that these rules don't discharge any premises.
As you say, adding intuitionistic reductio makes classical reductio derivable, so then you're home free.
But I think maybe I didn't express clearly enough what the rules were supposed to be. Intuitionistic reductio is the following (where \bot is the absurdity primitive):
From: G, A |- \bot
To: G |- ¬A
Classical reductio:
From: G, ¬A |- \bot
To: G |- A
There is a third rule, EFQ:
From: G |- \bot
To: G |- A
Prawitz uses /only/ the last rule in his intuitionistic system. But in his system ¬ is defined by implication and \bot, so the intuitionistic reductio is just an instance of conditional proof.
more tips here best replica designer bags go to the website gucci replica Full Report replica bags online
ReplyDelete