Database: Negation introduction

Inference rule 49: 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: Inference, entailment
  2. Terminology: Inference rule
  3. Definition: Negation