Why an inconsistent formal system can prove everything?

If $T$ is an inconsistent set of first order theorems (or axioms for the proof), then it is possible to prove from $T$ for some $\alpha$ both $\alpha$ and $\neg \alpha$. So without the loss of generality we can assume that $T$ includes $\alpha$ and $\neg\alpha$.

Now suppose that $\beta$ is whatever first order sentence that you want to prove.

1. $\alpha$ (in $T$)
2. $\beta \to \alpha$ (easily verified to be true since $\alpha$ is an axiom of $T$)
3. $\neg \alpha \to \neg \beta$ (Contrapositive Law)
4. $\neg \alpha$ (axiom of $T$)
5. $\neg \beta$ (inferred from 3 & 4)
6. $\neg \beta \to \alpha$ (holds for the same reason in 2, further more we have $\neg\beta$)
7. $\neg \alpha \to \neg\neg\beta$
8. $\neg \neg \beta$ (inferred from 4,7)
9. $\neg \neg \beta \to \beta$ (tautology)
10. $\beta$ (inferred from 8,9)

So you see, you can prove pretty much anything you want from $\\{\alpha ,\neg\alpha\\}$ for some first order sentence $\alpha$.

It doesn't have to: logics which don't are called paraconsistent.

The most important paraconsistent logic is relevance logic, which repudiates the K axiom: $$\alpha \rightarrow (\beta \rightarrow \alpha)$$ and replaces it by axioms that do not allow there to be unused assumptions. This is equivalent to saying weakening, the principle that if $\Gamma \vdash \alpha$ then $\Gamma'\vdash \alpha$ for $\Gamma\subset\Gamma'$. This blocks derivations such as Weltschmertz's, which appeals to the K axiom once, Asaf's which uses it twice; Francesco appeals to monotonicity in his proof, which is another name for weakening.

It's not difficult to see that this also blocks proofs of everything from a contradictory pair of propositions in a logic satisfying compactness, since one can prove inductively about such proof systems that if $\alpha\rightarrow\beta$, then all positive atoms in $\beta$ must occur either negatively in $\beta$ or positively in $\alpha$. So if our contradictory pair (over an assumption) takes the form $\alpha\rightarrow\beta$ and $\alpha\rightarrow\neg\beta$, we need to prove for any $\gamma$ that $\alpha\rightarrow\gamma$. But if we choose $\gamma$ to be any positive atom not occuring in $\alpha$, our inductive proof tells us this cannot be done. We need compactness here, to be ensure that the basis for all contradictory pairs can be expressed by a finitary formula.

From my recollection, it goes something like this: if $K$ is a first-order inconsistent theory, there exists, by definition, a formula $C$ such that $\vdash_{K} C$ and $\vdash_{K}\neg C$. If $D$ is an arbitrary formula in $K$ then we have the following chain (proof):

1. $C$
2. $\neg C$
3. $\neg C \Rightarrow (C\Rightarrow D)$ (Tautology)
4. $C \Rightarrow D$ (2,3, Modus Ponens)
5. $D$ (1,4, Modus Ponens).

Now, if inconsistency is defined the same way for logics of any other order, I think this proof wouldn't change. I don't see anything explicit about first-orderness in it, but correct me if I'm wrong.