Negation introduction

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: $(P\rightarrow Q)\land (P\rightarrow \neg Q)\leftrightarrow \neg P$

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 "When the phone rings I get happy" and then later state "When the phone rings I get annoyed", the logical inference which is made from this contradictory information is that the person is making a false statement about the phone ringing.

Proof


Step	Proposition	Derivation
1	$(P\to Q)\land (P\to \neg Q)$	Given
2	$(\neg P\lor Q)\land (\neg P\lor \neg Q)$	Material implication
3	$((\neg P\lor Q)\land \neg P)\lor ((\neg P\lor Q)\land \neg Q)$	Distributivity
4	$((\neg P\lor Q)\lor ((\neg P\lor Q)\land \neg Q))\land (\neg P\lor ((\neg P\lor Q)\land \neg Q))$	Distributivity
5	$\neg P\lor ((\neg P\lor Q)\land \neg Q)$	Conjunction elimination (4)
6	$\neg P\lor ((\neg P\land \neg Q)\lor (Q\land \neg Q))$	Distributivity
7	$\neg (Q\land \neg Q)$	Law of noncontradiction
8	$\neg P\lor (\neg P\land \neg Q)$	Disjunctive syllogism (5,6)
9	$(\neg P\lor \neg P)\land (\neg P\lor \neg Q)$	Distributivity
10	$\neg P\lor \neg P$	Conjunction elimination (7)
11	$\neg P$	Idempotency of disjunction

gollark: I suppose the best ways to get around that would be to... either specify a power which is small and not very useful so they won't meddle with it much, specify one which *seems* small and non-useful but isn't, rigorously and precisely specify a useful one, or just get some sort of ridiculously meta power.

gollark: Why would the person before you make there be a side effect? Just being spiteful and annoying?

gollark: You can actually run it in one of the many CC emulators which run out of the game, too, and this is where I do much of the testing.

gollark: Also it's entirely stored on pastebin and has no version control and is split across probably 15 different files.

gollark: I added a thing where I can remote into potatOS computers for... definitely debugging purposes... and run code, which makes it much easier to patch sandbox escapes where silly triangles don't release the code.

References

Wansing, Heinrich, ed. (1996). Negation: A Notion in Focus. Berlin: Walter de Gruyter. ISBN 3110147696.
Haegeman, Lilliane (30 Mar 1995). The Syntax of Negation. Cambridge: Cambridge University Press. p. 70. ISBN 0521464927.

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.

[1] Wansing, Heinrich, ed. (1996). Negation: A Notion in Focus. Berlin: Walter de Gruyter. ISBN 3110147696.

[2] Haegeman, Lilliane (30 Mar 1995). The Syntax of Negation. Cambridge: Cambridge University Press. p. 70. ISBN 0521464927.