Why an inconsistent formal system can prove everything? I am reading a Set Theory book by Kunen. He presents first-order logic and claims that if a set of sentences in inconsistent, then it proves every possible sentence. Since he does not explicitly specify the inference rules, I became curious as to how fundamental this property of inconsistent systems is.
So my question is what is the simplest proof, with the least use of assumptions, of the vague claim that "inconsistent systems can prove anything" - in particular I'm interested in the assumptions about the system needed to prove this - is it true only for first order logic? Only for first order logic with the "standard" rules of inference (Modus ponens and GEN)? Or is it such a basic truth that it can be proved for every "reasonable" proof system (and what is "reasonable")?
 A: 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):


*

*$C$

*$\neg C$

*$\neg C \Rightarrow (C\Rightarrow D)$ (Tautology)

*$C \Rightarrow D$ (2,3, Modus Ponens)

*$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.
A: If you assume natural deduction, this is easy to explain. Let $\Sigma$ be an inconsistent set of axioms. This means you can prove both $\phi$ and $\lnot\phi$ for some statement $\phi$: in symbols $\Sigma\vdash\phi$ and $\Sigma\vdash\lnot\phi$. Now you suppose the negation of whatever statement $\psi$ you like to prove, but since, by monotonicity, $\Sigma\cup\{\lnot\psi\}\vdash\phi$ and $\Sigma\cup\{\lnot\psi\}\vdash\lnot\phi$, you can apply negation elimination obtaining $\Sigma\vdash\psi$.
A: 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.


*

*$\alpha$ (in $T$)

*$\beta \to \alpha$ (easily verified to be true since $\alpha$ is an axiom of $T$)

*$\neg \alpha \to \neg \beta$ (Contrapositive Law) 

*$\neg \alpha$ (axiom of $T$)

*$\neg \beta$ (inferred from 3 & 4)

*$\neg \beta \to \alpha$ (holds for the same reason in 2, further more we have $\neg\beta$)

*$\neg \alpha \to \neg\neg\beta$

*$\neg \neg \beta$ (inferred from 4,7)

*$\neg \neg \beta \to \beta$ (tautology)

*$\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$.
A: 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.
