Prove that a formal system is absolutely inconsistent I'm using the book An Introduction to Mathematical Logic and Type Theory: To Truth Through Proof, and it does not have any solutions and barely any examples. I want to understand how to prove that all wff are theorems. Here is one exercise. 

Let $\Lambda$ be a formulation of propositional calculus in which the sole connective are negation and disjunction, the sole rule of inference is Modes Ponens, and with the following axiom schema: $\sim[A\vee B]\vee[B\vee C] $. Prove that $\Lambda$ is absolutely inconsistent.

I know that I need to prove that every wffs is a theorem with only the rule "if $A$ and $\sim A \vee B$  are theorems, B is a theorem" and the above axiom. 
Now, let $F$ be a wff, how do I prove it's a theorem, where do I even start?
 A: First, let's find a proof of $X$ where $X$ is a propositional variable rather than an arbitrary formula. Afterwards, if want to prove an arbitrary wff $A$, we can take our proof of $X$ and replace every $X$ in that proof with $A$. This works because the system we're working with here has no axioms or inference rules that allow us to do something with a propositional variable that we can't also do with a more complex formula.
We can find a proof of $X$ from the conclusion up by a sort of semi-smart brute force search. Every premise we need must be concluded either by modus ponens or as an instance of the axiom scheme, so whenever we need does not have the right shape to be an instance of the axiom, it must be concluded by modus ponens.
This is, for example, the case for the final conclusion $X$, so the last step in the proof must be modus ponens. We then have to prove
$$ {\sim} A \lor X  \qquad\text{and}\qquad A $$
for some $A$ whose structure we're free to choose. The first of these cannot be an axiom no matter which $A$ we choose, so it itself must be concluded by modus ponens. So what we now need to prove is
$$ {\sim}B \lor [{\sim}A\lor X] \qquad\qquad B  \qquad\qquad A $$
The first one of these looks promising because it will be an instance of the axiom if only we decide that $B$ is going to be $C\lor{\sim}A$. That leaves us with the following to prove:
$$ C\lor{\sim}A  \qquad\qquad A $$
The first of these again needs to be proved by modus ponens (the negation is in the wrong place and we don't have any rule saying that $\lor$ is commutative), so we need
$$ {\sim}D \lor [C\lor {\sim}A] \qquad\qquad D \qquad\qquad A $$
and the first of these becomes an axiom if $D$ is $E\lor C$. That coverts our proof obligations to
$$ E\lor C \qquad\qquad A $$
and these can both be axioms by choosing appopriate unfoldings for $E$, $C$, and $A$, namely


*

*$A = {\sim}[X\lor X]\lor [X\lor X]$

*$E = {\sim}[X\lor X]$

*$C = X\lor X$


Putting everything together we can write down our proof in standard order:


*

*$~{\sim}[X\lor X]\lor [X\lor X] \qquad$ (axiom)

*$A \qquad$ (1, definition of $A$)

*$E\lor C \qquad$ (1, definition of $E$ and $C$)

*${\sim}[E\lor C]\lor[C\lor {\sim}A] \qquad$ (axiom)

*$C \lor {\sim}A \qquad$ (3, 4, MP)

*${\sim}[C\lor {\sim}A]\lor[{\sim}A\lor X] \qquad$(axiom)

*${\sim}A\lor X \qquad$ (5, 6, MP)

*$X \qquad$ (2, 7, MP)

