Exercises

Skip to main content

Cornell University PRL Project

PRL Home Introduction Math Library Publications Projects System

Seminar People The Book Lectures Other Groups

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.