Logical Investigations, with the Nuprl Proof Assistant
Robert L. Constable and Anne Trostle July 2014Table of Contents
- Introduction
- The Minimal Implicational Calculus
- False Propositions and Negation
- Conjunction and Disjunction
- Theorem 9: (P ∨ ∼P) ⇒ (∼∼P ⇒ P)
- Theorem 10: ∼∼(P ∨ ∼P)
- Theorem 11: ((∼P) ∨ (∼Q)) ⇒ ∼(P ∧ Q)
- Theorem 12: ∼(P ∨ Q) ⇒ ((∼P) ∧ (∼Q))
- Theorem 13: ((∼P) ∧ (∼Q)) ⇒ ∼(P ∨ Q)
- Exercises
- First-Order Logic: All and Exists
- Theorem 17a: (C ⇒ (∀x:T. (P x))) ⇒ (∀x:T. (C ⇒ (P x)))
- Theorem 17b: (∀x:T. (C ⇒ (P x))) ⇒ (C ⇒ (∀x:T. (P x)))
- Theorem 18a: ((∃x:T. (P x)) ⇒ C) ⇒ (∀x:T. ((P x) ⇒ C))
- Theorem 18b: (∀x:T. ((P x) ⇒ C)) ⇒ ((∃x:T. (P x)) ⇒ C)
- Theorem 19a: (C ∨ (∼C)) ⇒ (∃x:T. True) ⇒ (C ⇒ (∃x:T. (P x))) ⇒ (∃x:T. (C ⇒ (P x)))
- Theorem 19b: (∃x:T. (C ⇒ (P x))) ⇒ (C ⇒ (∃x:T. (P x)))
- Theorem 20a: (C ∨ (∼C)) ⇒ (∃x:T. True) ⇒ ((∼(∀x:T. (P x))) ⇒ (∃x:T. (∼(P x)))) ⇒
((∀x:T. (P x)) ⇒ C) ⇒ (∃x:T. ((P x) ⇒ C)) - Theorem 20b: (∃x:T. ((P x) ⇒ C)) ⇒ ((∀x:T. (P x)) ⇒ C)
- Exercises
- 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)
- Appendix A: How to Step through a Proof
- Appendix B: Answers to Exercises
- References