//
Skip to main content
PRL Project

Logical Investigations, with the Nuprl Proof Assistant
Table of Contents

Previous Page Next Page

Theorem 11: ((∼P) ∨ (∼Q)) ⇒ ∼(PQ)


∀[P,Q:ℙ].(((¬P) ∨ (¬Q)) ⇒ (¬(P ∧ Q))) Extract: λf,g. let p,q = g in case f of inl(np) => np p | inr(nq) => nq q where f : (¬P) ∨ (¬Q) g : P ∧ Q p : P q : Q np : ¬P ≡ (P ⇒ False) nq : ¬Q ≡ (Q ⇒ False)

This theorem relates conjunction and disjunction and is part of a group of relations known as De Morgan's laws. Unlike the next relation (Theorem 12), we cannot constructively prove the reverse direction of this theorem.


Nuprl Proof


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




Previous Page Next Page


Table of Contents