tag:blogger.com,1999:blog-4787751963956773800.post8994739295951542690..comments2014-12-15T00:47:53.658-08:00Comments on Modern Materialism: Independence of ReductioMichael Johnsonhttp://www.blogger.com/profile/01746105737592972675noreply@blogger.comBlogger3125tag:blogger.com,1999:blog-4787751963956773800.post-85569776413176060592009-11-13T04:26:49.385-08:002009-11-13T04:26:49.385-08:00Hi,
Yes, you won't get classical logic by jus...Hi,<br /><br />Yes, you won't get classical logic by just including the intro and elim rules<br /><br />p / ~~p (~-intro)<br />~~p / p (~-elim)<br /><br />The crucial difference is that these rules don't discharge any premises.<br /><br />As you say, adding intuitionistic reductio makes classical reductio derivable, so then you're home free.<br /><br />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):<br /><br />From: G, A |- \bot<br />To: G |- ¬A<br /><br />Classical reductio:<br /><br />From: G, ¬A |- \bot<br />To: G |- A<br /><br />There is a third rule, EFQ:<br /><br />From: G |- \bot<br />To: G |- A<br /><br />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.Ole Thomassen Hjortlandhttps://www.blogger.com/profile/08574281945279890524noreply@blogger.comtag:blogger.com,1999:blog-4787751963956773800.post-28085866529961278212009-11-12T12:26:20.028-08:002009-11-12T12:26:20.028-08:00Ole,
Thanks for the reply. I guess I had assumed ...Ole,<br /><br />Thanks for the reply. I guess I had assumed the intro and elimination rules for negation were:<br /><br />p / ~~p (~-intro)<br />~~p / p (~-elim)<br /><br />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. <br /><br />I guess my worry was, as you say, that other rules one can add don't seem like either intro or elimination for negation.<br /><br />But I am confused by your distinction between classical reductio and intuitiionistic reductio. Your classical reductio is:<br /><br />From: G, A / B & ~B<br />To: G / ~A<br /><br />And your intuistionist reductio (EFQ) is:<br /><br />From: G / B & ~B<br />To: G / A<br /><br />And you suggest adding the former as ~-intro and the latter as ~-elim. But you can derive the latter from the former:<br /><br />1. G / B & ~B (by supposition)<br />2. ~A / ~A (by assumption)<br />3. G, ~A / ~A & (B & ~B) (&-intro, 1, 2)<br />4. G, ~A / B & ~B (&-elim, 3)<br />5. G / ~~A (classical reductio, 4)<br />6. G / A (double negation, 5)<br /><br />The derivation doesn't work without double negation, but once you have that, there's no reason for both rules, yes?<br /><br />But thanks, I think I'm generally clearer on these issues now. I should read up on intuitionistic logic.Michael Johnsonhttps://www.blogger.com/profile/01746105737592972675noreply@blogger.comtag:blogger.com,1999:blog-4787751963956773800.post-30255398109376611792009-11-12T02:17:59.674-08:002009-11-12T02:17:59.674-08:00Hi Michael,
The question is: which negation rules...Hi Michael,<br /><br />The 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.<br /><br />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.<br /><br />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 Thomassen Hjortlandhttps://www.blogger.com/profile/08574281945279890524noreply@blogger.com