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