2
$\begingroup$

I'd like to derive the following inference rule:

$$ \frac{p\lor(q\land\neg q)}{p}\quad\text{[ContradictionElimination]} $$

I assumed that I could do this minimally somehow, however it turns out I need an alternative form of the principle of explosion. My derivation is:

Rule (ContradictionElimination)
  Premise
    P∨(Q∧⌐Q)
  Conclusion
    P
  Proof
    Suppose
      P
    Hence
      P
    P=>P

    Suppose
      Q∧⌐Q
    Then
      Q
      ⌐Q
    Hence
      P by PrincipleOfExplosionAlternativeForm
    Q∧⌐Q=>P

    P by DisjunctionElimination

My alternative form of the principle of explosion is, by the way:

$$ \frac{p\quad\neg p}{q}\quad\text{[PrincipleOfExplosionAlternativeForm]} $$

This is easy enough to derive from the standard principle of explosion and modus ponens.

Without a way to eliminate contradictions minimally, so to speak, all my minimal proofs of De Morgan's laws become intuitionsitic. This seems wrong to me.

$\endgroup$
2
  • 1
    $\begingroup$ I think you messed up $\land$ and $\lor$ in the display formula $\endgroup$
    – Hagen von Eitzen
    Jun 17, 2016 at 18:20
  • $\begingroup$ You're right, thank you. $\endgroup$
    – James Smith
    Jun 17, 2016 at 18:27

2 Answers 2

Reset to default
0
$\begingroup$

I'm going to try to answer this question although I'm not entirely sure the answer is right. Maybe it will encourage debate, though. I think that the answer is no, you cannot derive this rule without some form of the principle of explosion. My reasoning goes as follows...

The premise is a disjunction $p\lor(q\land\neg q)$. I have chosen to arrive at the conclusion by proof by cases, disjunction elimination in other words, which means I have to deal with $q\land\neg q$ somehow. The only other way that I can see to make progress from the premise is to use the rule that distributes disjunction over conjunction. This gives $(p\lor q)\land(p\lor\neg q)$. Now I have two disjunctions to deal with. Taking the rightmost $p\lor q$, I can only proceed by proof by cases again. Assuming $p$, I'm done. Assuming $q$ on the other hand, I must make use of the other side of the conjunction, namely $p\lor\neg q$ and I must then proceed to $q\land(p\lor\neg q)$. Using the rule that conjunction distributes over disjunction I get, unfortunately, $(p\land q)\lor(q\land\neg q)$ and I'm no better of than where I started.

My line of reasoning is based on there only really being one way that the derivation can proceed. However it seems exhaustive, so I think there's something in it. It also seems, from an intuitive standpoint, that you can't eliminate $q\land\neg q$ without something like the principle of explosion, although admittedly this intuition is tainted by my findings above. Perhaps some other interpretation would shed more light on this.

$\endgroup$
7
  • $\begingroup$ Natural Deduction has a "basic" rule that is $\bot \vdash p$, where $\bot$ (the falsum) stands for a contradiction. Thus, it is exactly your $p , \lnot p \vdash q$. With this rule available, you derivation of the "Contradiction Elimination" rule by way of $\lor$-elimination is correct. $\endgroup$
    – Mauro ALLEGRANZA
    Jun 18, 2016 at 10:59
  • 1
    $\begingroup$ Great, thanks Mauro. Interesting to know that throwing away a contradiction can only be done intuitionistically, not minimally. $\endgroup$
    – James Smith
    Jun 18, 2016 at 13:11
  • $\begingroup$ As an aside, my implementation (for want of a better word) of propositional logic never needs $\bot$. The above derivation was the last one I needed to work out without it. I guess how you set things up is just a matter of taste. Anyway, I thought it worth a mention. $\endgroup$
    – James Smith
    Jun 18, 2016 at 13:13
  • 1
    $\begingroup$ Correct; see Minimal logic. $\endgroup$
    – Mauro ALLEGRANZA
    Jun 18, 2016 at 13:42
  • $\begingroup$ I'm showing signs of improvement! Thanks for all your help this last couple of weeks. $\endgroup$
    – James Smith
    Jun 18, 2016 at 13:45
-2
$\begingroup$

In Polish notation you might use the rule of inference

CN$\alpha$K$\beta$N$\beta$ $\vdash$ $\alpha$

which I'll call No.

I'll also use

Kol: K$\alpha$$\beta$ $\vdash$ $\alpha$

Kor: K$\alpha$$\beta$ $\vdash$ $\beta$

Ki: $\alpha$, $\beta$ $\vdash$ K$\alpha$$\beta$

and

Ao: A$\alpha$$\beta$, C$\alpha$$\gamma$, C$\beta$$\gamma$ $\vdash$ $\gamma$

The proof then can go:

premise   1 ApKqNq
suppose   2 | p
Ci 2-2    3 Cpp
suppose   4 | KqNq
suppose   5 || Np
Kol 4     6 || q
Kor 4     7 || Nq
Ki 6 7    8 || KqNq
Ci 5-8    9 | CNpKqNq
No 9      10 | p
Ci 4-10   11 CKqNqp
Ao 1 3 11 12 p
$\endgroup$
2
  • $\begingroup$ I don't think this is going to help much. Your No. rule, which translates into $\neg\alpha\rightarrow(\beta\land\neg\beta)\Rightarrow\alpha$, pretty much assumes the very thing I'm trying to prove as far as I can tell. It is couched slightly differently, but essentially says if $\neg\alpha$ "implies" (here I use the word reservedly) a contradiction, then $\alpha$ holds. This is hardly different from my own rule, the only difference being that material consequence has replaced conjunction. If your derivation relies on this rule at the last step, I don't think it will help much. $\endgroup$
    – James Smith
    Jun 18, 2016 at 5:40
  • $\begingroup$ @James Smith I thought you wanted to prove "From a disjunction of p and a contradiction, we can infer p". My rule doesn't have a disjunction in it. So, I don't know why you think it hardly different from your rule. Also, the rule No above ends up stronger than the principle of explosion, as it can probably replace any other negation elimination and introduction rules in your natural deduction system, while the principle of explosion probably can't do that. $\endgroup$
    – Doug Spoonwood
    Jun 18, 2016 at 13:20

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .