Database: Negation introduction

Inference rule 64: Negation introduction (declared)

Given that \phi entails \psi , and that \phi entails the negation \neg \psi , we may infer that the negation \neg \phi holds: \cfrac{\phi \vdash \psi \quad \phi \vdash \neg \psi}{\vdash \neg \phi}.

This database entry builds on the following:

  1. Terminology: Class, statement
  2. Definition: Negation
  3. Terminology: Inference
  4. Terminology: Entailment
  5. Terminology: Inference rule