Non contradiction principle

Question

I want to know where do come exactly the contradiction principle and if a formal proof system needs it to work. Have you some books references who talks about it ?

Answer 1

The motive for $p\land\neg p$ not being true is that,

1. if from $p\land\neg p$ you can deduce $(p\lor q)\land\neg p$, and
2. if from $(p\lor q)\land\neg p$ you can in turn deduce $q$,

you can prove anything. This phenomenon, called "explosion", makes for a logic that is neither useful nor interesting.

A logic in which a contradiction doesn't lead to explosion is called paraconsistent or Brazilian, and requires the rules of inference to be weakened enough that at least one of the above steps is invalid.