Negation World

theorem RTPNotes.Worlds.Negation.level1 {P : Prop} : False → P

Level 1

For any proposition P, the implication False → P is true.

theorem RTPNotes.Worlds.Negation.level2 {P : Prop} : ¬P → P → False

Level 2

For any proposition P, if ¬ P and P are both true, then we obtain a proof of False.

theorem RTPNotes.Worlds.Negation.level3 {P : Prop} : P → ¬¬P

Level 3

For any proposition P, P → ¬ ¬ P.

theorem RTPNotes.Worlds.Negation.level4 {P : Prop} : ¬(P ∧ ¬P)

Level 4

For any proposition P, ¬ (P ∧ ¬ P).

theorem RTPNotes.Worlds.Negation.level5 {P Q : Prop} : P → ¬P → Q

Level 5

It is possible to prove any proposition Q from the hypothesis that both P and ¬ P are true.

theorem RTPNotes.Worlds.Negation.level6 {P Q : Prop} : (P → Q) → ¬Q → ¬P

Level 6

For any propositions P and Q, if P → Q holds then ¬ Q → ¬ P also holds.

theorem RTPNotes.Worlds.Negation.level7 {P Q : Prop} : P ∧ ¬Q → ¬(P → Q)

Level 7

For any propositions P and Q, if P is true and Q is false, then P → Q is not true.

theorem RTPNotes.Worlds.Negation.level8 {P Q : Prop} : ¬(P ∨ Q) ↔ ¬P ∧ ¬Q

Level 8

For any propositions P and Q, the propositions ¬ (P ∨ Q) and ¬ P ∧ ¬ Q are logically equivalent.

theorem RTPNotes.Worlds.Negation.level9 {P Q : Prop} : ¬P ∨ ¬Q → ¬(P ∧ Q)

Level 9

For any propositions P and Q, if P is false or Q is false then P ∧ Q is false.

theorem RTPNotes.Worlds.Negation.level10 {P : Prop} : ¬P ↔ ¬¬¬P

Level 10

For any proposition P, ¬ P is logically equivalent to ¬ ¬ ¬ P.

theorem RTPNotes.Worlds.Negation.level11 {P : Prop} : P ∨ ¬P → ¬¬P → P

Level 11

The law of excluded middle implies double negation elimination: for any proposition P, P ∨ ¬ P implies ¬ ¬ P → P.