Introdução da Negação

Introdução da negação é uma Regra de Inferência ou Regra de Transformação, no campo do cálculo preposicional.

A introdução da negação é uma regra que diz que se um elemento antecedente implica tanto no consequente como na sua negação, significa que o antecedente é uma contradição.

Notação Formal

Pode ser escrito como: $(P\to Q)\wedge (P\to \mathrm{\neg }Q)\leftrightarrow \mathrm{\neg }P$

Uma de muitas formas de utilizar a introdução da negação é usada quando queremos provar duas declarações contraditórias a partir de um único fato. Por exemplo, se uma pessoa diz que "quando o telefone toca, eu fico feliz" e depois diz que "quando o telefone toca, eu fico irritado". A inferência lógica que podemos fazer a partir dessa contradição é que a pessoa está fazendo uma falsa declaração sobre quando o telefone toca.