Principle of explosion: Other arguments?

Question

I've come across a proof-theoretic argument for explosion on Wikipedia, which is as follows:

1. $A \ \ \wedge\sim A$

2. $A$

3. $ \sim A$

4. $ A \lor B$

5. $B$

6. $(A \ \ \wedge \sim A) \implies B$

I've thought of another argument, which isn't on the same Wikipedia page as the above. As far as I can see, it is valid but I would like to see your opinions. Perhaps you could provide me with some more (relatively simple) arguments for explosion within classical logic?

1. $A \ \ \wedge\sim A$

2. $A$

3. $A \lor B$

4. $ \sim A$

5. $B$

6. $(A \ \ \wedge \sim A) \implies B$

Answer 1

I use Polish/Lukasiewicz notation. The rule of Negation elimination that I use says that from N$\beta$ having the same scope as an instance of K$\alpha$N$\alpha$ we can infer $\beta$.

assumption                   1 | KaNa
assumption                   2 || Nb
2, 1 Negation Elimination    3 | b
1-3 Conditional Introduction 4 CKaNab.

As a more axiomatic proof, I'll assume that we have the following three axioms:

A1 CpCqp.
A2 CCpCqrCCpqCpr.
A3 CCNpKqNqp.

Then, with Dx.y indicating the condensed detachment with x as the major premise and as the minor premise we can proceed as follows:

assumption                   1 | KaNa
assumption                   2 || Nb
D[A1].1                      3 || CpKaNa
D3.3                         4 || KaNa
2-4 Conditional Introduction 5 | CNbKaNa
D[A3].5                      6 | b

Or as follows:

assumption                   1 | KaNa
D[A1].1                      2 | CpKaNa
D[A3].2                      3 | p

Thus, a fully axiomatic proof can proceed as follows:

axiom 1 CpCqp.
axiom 2 CCpCqrCCpqCpr.
axiom 3 CCNpKqNqp.
D1.3  4 CpCCNqKrNrq.
D2.4  5 CCpCNqKrNrCpq.
D5.1  6 CKpNpq.

Answer 2

Here's a 23 step OTTER proof from the 21 letter single axiom of Meredith CCCCCpqCNrNsrtCCtpCsp.

-----> EMPTY CLAUSE at  11.77 sec ----> 7420 [hyper,2,7233] $F.

Length of proof is 23.  Level of proof is 17.

---------------- PROOF ----------------

1 [] -P(C(x,y))| -P(x)|P(y).
2 [] -P(C(N(C(p,N(N(p)))),q)).
3 [] P(C(C(C(C(C(x,y),C(N(z),N(u))),z),v),C(C(v,x),C(u,x)))).
4 [hyper,1,3,3] P(C(C(C(C(x,y),C(z,y)),C(y,u)),C(v,C(y,u)))).
6 [hyper,1,3,4] P(C(C(C(x,C(N(y),z)),u),C(y,u))).
14 [hyper,1,3,6] P(C(C(C(x,x),y),C(z,y))).
16 [hyper,1,14,14] P(C(x,C(y,C(z,z)))).
19 [hyper,1,3,14] P(C(C(C(x,y),N(y)),C(z,N(y)))).
23 [hyper,1,3,16] P(C(C(C(x,C(y,y)),z),C(u,z))).
96 [hyper,1,3,23] P(C(C(C(x,y),z),C(y,z))).
106 [hyper,1,3,96] P(C(C(C(C(N(x),N(y)),x),z),C(y,z))).
111 [hyper,1,96,3] P(C(x,C(C(x,y),C(z,y)))).
113 [hyper,1,96,111] P(C(x,C(C(C(y,x),z),C(u,z)))).
247 [hyper,1,106,96] P(C(x,C(N(x),y))).
250 [hyper,1,106,19] P(C(x,C(y,N(N(x))))).
340 [hyper,1,96,247] P(C(x,C(N(C(y,x)),z))).
405 [hyper,1,96,340] P(C(x,C(N(C(y,C(z,x))),u))).
493 [hyper,1,3,113] P(C(C(C(C(C(x,C(C(C(y,z),C(N(u),N(v))),u)),w),C(v6,w)),y),C(v,y))).
1660 [hyper,1,3,493]     P(C(C(C(x,y),C(z,C(C(C(y,u),C(N(v),N(x))),v))),C(w,C(z,C(C(C(y,u),C(N(v),N(x))),v))))).
5524 [hyper,1,1660,111] P(C(x,C(C(C(y,z),u),C(C(C(z,v),C(N(u),N(y))),u)))).
5540 [hyper,1,5524,5524] P(C(C(C(x,y),z),C(C(C(y,u),C(N(z),N(x))),z))).
5609 [hyper,1,5540,3] P(C(C(C(x,y),C(N(C(C(x,z),C(u,z))),N(C(C(C(z,v),C(N(w),N(u))),w)))),C(C(x,z),C(u,z)))).
6115 [hyper,1,5609,405] P(C(C(x,C(x,y)),C(z,C(x,y)))).
7172 [hyper,1,6115,250] P(C(x,C(y,N(N(y))))).
7189 [hyper,1,7172,7172] P(C(x,N(N(x)))).
7233 [hyper,1,247,7189] P(C(N(C(x,N(N(x)))),y)).
7420 [hyper,2,7233] $F.

------------ end of proof -------------