Is it possible to eliminate a contradiction without recourse to the principle of explosion?

Question

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.

Answer 1

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

Answer 2

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.