Skip to main content
PRL Project

Logical Investigations, with the Nuprl Proof Assistant
Table of Contents

Previous Page Next Page

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.