Database: Law of Noncontradiction

Theorem 65: 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: Class, statement
  2. Definition: Conjunction
  3. Definition: Negation
  4. Terminology: Inference
  5. Terminology: Entailment
  6. Terminology: Inference rule
  7. Inference rule: Conjunction elimination
  8. Inference rule: Negation introduction