Logical Investigations, with the Nuprl Proof Assistant
Table of Contents
Theorem 11: ((∼P) ∨ (∼Q)) ⇒ ∼(P ∧ Q)
∀[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
 View the proof in PDF format
 Step through the proof in the frame:
Table of Contents