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 ?
The motive for $p\land\neg p$ not being true is that,
- if from $p\land\neg p$ you can deduce $(p\lor q)\land\neg p$, and
- 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.