Heads up. I have no technical training in logic, nor have read any book about it. This question is coming mostly from my intuition, so please consider giving me a reference --- I'm particularly interested in technical explanations to the fact that contradictions trivialize mathematics.
I'm trying to make sure that the following proof is correct and what it says for mathematics. (In this question, whenever I say "mathematics", I mean the systems of logic that express mathematics.)
Theorem. (P and ~P) implies Q.
Proof. Suppose P and ~P. Then
1 P detachment from P and ~P
2 ~~P double negation
3 ~~P or Q disjunction introduction
4 ~P implies Q implication?
5 ~P detachment from P and ~P
6 Q modus ponens
In other words, a contradiction implies anything at all.
Question 1. Is this why we cannot have contradictions in mathematical logic (and therefore in mathematics)? Because --- as Eric Wolsey comments below --- sentential logic is a subset of predicate logic (and, perhaps I may add that mathematics is expressed by a predicate logic), then we may say that the theorem above says that if mathematics would have a contradiction, then anything at all would be implied by it. (Apparently the answer to this question is "yes, the theorem above is correct and it is enough of a reason to say mathematics cannot allow a contradiction".
Question 2. I'm concerned with speaking nonsense here. The relationship between these logic systems are not very clear to me, so my second question would be --- what book or paper would spell this result in particular? I'd like to read the exposition of an expert. (So this is a reference request.)