The Logic Behind the Logic

Proof by contradiction rests on the law of the excluded middle: every statement is either true or false, with no third option. If "not X" leads to nonsense, then "not X" is false, so X must be true.

This seems obvious, but it is not innocent. In the 1900s, logicians showed that in certain systems some statements are neither provable nor refutable — Gödel's incompleteness theorems are the famous example. The method also powers computer science: SAT-solvers, used in circuit design and software verification, run contradiction-search at industrial scale.