TITLE: Principle of explosion: Other arguments?
QUESTION [3 upvotes]: I've come across a proof-theoretic argument for explosion on Wikipedia, which is as follows:

$A \ \ \wedge\sim A$
$A$
$ \sim A$
$ A \lor B$
$B$
$(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?

$A \ \ \wedge\sim A$
$A$
$A \lor B$
$ \sim A$
$B$
$(A \ \ \wedge \sim A) \implies B$

REPLY [0 votes]: 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 -------------
{"set_name": "stack_exchange", "score": 3, "question_id": 1120251}