Logical Investigations, with the Nuprl Proof Assistant
Table of Contents
Exercises
Show the proof and find the extract of the evidence for the following theorems:
- Theorem 21a: (∃x:T. True) ⇒ ((∃x:T. (P x)) ∨ C) ⇒ (∃x:T. ((P x) ∨ C))
- Theorem 21b: (∃x:T. ((P x) ∨ C)) ⇒ ((∃x:T. (P x)) ∨ C)
- Theorem 22a: ((∀x:T. (P x)) ∨ C) ⇒ (∀x:T. ((P x) ∨ C))
- Theorem 22b: (C ∨ (∼C)) ⇒ (∀x:T. ((P x) ∨ C)) ⇒ ((∀x:T. (P x)) ∨ C)
- Theorem 23a: ((∃x:T. (P x)) ∧ C) ⇒ (∃x:T. ((P x) ∧ C))
- Theorem 23b: (∃x:T. ((P x) ∧ C)) ⇒ ((∃x:T. (P x)) ∧ C)
- Theorem 24a: ((∀x:T. (P x)) ∧ C) ⇒ (∀x:T. ((P x) ∧ C))
- Theorem 24b: (∃x:T. True) ⇒ (∀x:T. ((P x) ∧ C)) ⇒ ((∀x:T. (P x)) ∧ C)
Answers to exercises are shown in Appendix B.