Negation introduction

Negation introduction is a rule of inference, or transformation rule, in the field of propositional calculus. Negation introduction is a rule of inference, or transformation rule, in the field of propositional calculus. Negation introduction states that if a given antecedent implies both the consequent and its complement, then the antecedent is a contradiction. This can be written as: ( P → Q ) ∧ ( P → ¬ Q ) ↔ ¬ P {displaystyle (P ightarrow Q)land (P ightarrow eg Q)leftrightarrow eg P}