Logical rule of inference
Negation introductionType | Rule of inference |
---|
Field | Propositional calculus |
---|
Statement | If a given antecedent implies both the consequent and its complement, then the antecedent is a contradiction. |
---|
Symbolic statement | ![{\displaystyle (P\rightarrow Q)\land (P\rightarrow \neg Q)\rightarrow \neg P}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a0797e0b37adf477d22ef663297e4c7b470e6630) |
---|
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.[1][2]
Formal notation
This can be written as:
An example of its use would be an attempt to prove two contradictory statements from a single fact. For example, if a person were to state "Whenever I hear the phone ringing I am happy" and then state "Whenever I hear the phone ringing I am not happy", one can infer that the person never hears the phone ringing.
Many proofs by contradiction use negation introduction as reasoning scheme: to prove ¬P, assume for contradiction P, then derive from it two contradictory inferences Q and ¬Q. Since the latter contradiction renders P impossible, ¬P must hold.
Proof
Step
|
Proposition
|
Derivation
|
1 |
![{\displaystyle (P\to Q)\land (P\to \neg Q)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/a6a2dc625c0759664e78ad6f730addac5f05be34) |
Given
|
2 |
![{\displaystyle (\neg P\lor Q)\land (\neg P\lor \neg Q)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/4dbc51bf092407d429a36bac0c6313f2e05e1b49) |
Material implication
|
3 |
![{\displaystyle \neg P\lor (Q\land \neg Q)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/cd943fec25e689ff11bb8fff3135a4de2d9cd23f) |
Distributivity
|
4 |
![{\displaystyle \neg P\lor F}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8f9f122ada717873883029719ab9d31cd86235b3) |
Law of noncontradiction
|
5 |
![{\displaystyle \neg P}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5eb0d6c8752f8c7256d69c62e77dfe4c466dbe58) |
Disjunctive syllogism (3,4)
|
See also
References