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