//
Skip to main content
PRL Project

Logical Investigations, with the Nuprl Proof Assistant
Table of Contents

Previous Page Next Page

Theorem 12: ∼(PQ) ⇒ ((∼P) ∧ (∼Q))


∀[P,Q:ℙ].((¬(P ∨ Q)) ⇒ ((¬P) ∧ (¬Q))) Extract: λf.⟨λp.(f (inl p)), λq.(f (inr q))⟩ where f : ¬(P ∨ Q) ≡ ((P ∨ Q) ⇒ False) p : P q : Q

This theorem is another relation from De Morgan's laws and is one that we can constructively prove in the reverse direction as well (Theorem 13).

Nuprl Proof


⊢ ∀[P,Q:ℙ]. ((¬(P ∨ Q)) ⇒ ((¬P) ∧ (¬Q))) | BY RepeatFor 2 ((UD THENA Auto)) | [1]. P: ℙ [2]. Q: ℙ ⊢ (¬(P ∨ Q)) ⇒ ((¬P) ∧ (¬Q)) | BY (D 0 THENA Auto) ⇒ Construction rule | 3. ¬(P ∨ Q) ⊢ (¬P) ∧ (¬Q) | BY (D 0 THENA Auto) ∧ Construction rule |\ | ⊢ ¬P Subgoal 1: Prove (¬P) | | 1 BY (D 0 THENA Auto) ⇒ Construction rule; definition of negation | | | 4. P | ⊢ False | | 1 BY (Unfold `not` 3 THEN D 3) ⇒ Application rule on ((P ∨ Q) ⇒ False) | |\ | | 3. P | | ⊢ P ∨ Q Subgoal 1.1: Prove (P ∨ Q) | | | 1 2 BY (OrLeft THENA Auto) ∨ Construction rule: Prove the left side | | | | | ⊢ P | | | 1 2 BY NthHyp 3 Hypothesis rule | \ | 3. P | 4. False | ⊢ False Subgoal 1.2: Show False, with assumption of False now available | | 1 BY NthHyp 4 Hypothesis rule \ ⊢ ¬Q Subgoal 2: Prove (¬Q) | BY (D 0 THENA Auto) ⇒ Construction rule; definition of negation | 4. Q ⊢ False | BY (Unfold `not` 3 THEN D 3) ⇒ Application rule on ((P ∨ Q) ⇒ False) |\ | 3. Q | ⊢ P ∨ Q Subgoal 2.1: Prove (P ∨ Q) | | 1 BY (OrRight THENA Auto) ∨ Construction rule: Prove the right side | | | ⊢ Q | | 1 BY NthHyp 3 Hypothesis rule \ 3. Q 4. False ⊢ False Subgoal 2.2: Show False, with assumption of False now available | BY NthHyp 4 Hypothesis rule




Previous Page Next Page


Table of Contents