Database: Law of Noncontradiction

Theorem 50: Law of Noncontradiction (inference rule)

We may (from no premises at all) infer that the negation of the conjunction of \phi and its negation \neg \phi holds: \cfrac{}{\vdash \neg (\phi \wedge \neg \phi)}.

Proof: Assume \phi \wedge \neg \phi . Using conjunction elimination twice, we infer that \phi holds and that \neg \phi holds. But then we have inferred the entailments (\phi \wedge \neg \phi) \vdash \phi \hspace{3mm} \textup{and} \hspace{3mm} (\phi \wedge \neg \phi) \vdash \neg \phi, meaning we may infer by negation introduction that \neg (\phi \wedge \neg \phi) holds. \square

This database entry builds on the following:

  1. Terminology: Inference, entailment
  2. Terminology: Inference rule
  3. Definition: Conjunction
  4. Definition: Negation
  5. Inference rule: Conjunction elimination
  6. Inference rule: Negation introduction