| 1. |
Historical studies: |
| |
- Read about the origins of first-order logic in From Frege to Gödel
and relate to our account in class.
|
| |
Read about the controversy over the law of excluded middle.
There is good material on the Web. |
| 2. |
Develop first-order logic as a Hilbert system. See books such as A. Church,
Introduction to Mathematical Logic, Vol I. Compare to tableau.
|
| 3. |
Develop propositional logic from the start using refinement logic by rewriting Smullyan, p. 15-17.
|
| 4. |
Write up a complete account of our treatment of order and algebraic structures in first-order logic.
|
| 5. |
Give a proof that first-order monadic predicate logic is decidable.
|
| 6. |
Prove Church's theorem that validity in first-order logic is not decidable by formalizing
Turing machines or a simple programming language.
|
| 7. |
Using refinement logic with primitive recursive functions over Z (lambda-PRL), prove some
interesting program correct. Read the article Proofs as Program, by Bates and
Constable (see Nuprl Web page).
|
| 8. |
Interactions with the PRL research group. Various researchers are willing to talk with you
about specific projects: |
| |
- Reflection in first-order logic, a topic that leads to Tarski's theorem about the
undefinability of truth. Contact Eli Barzilay (eli@cs.cornell.edu).
|
| |
The towers of Hanoi problem stated and solved as a theorem. Contact Dr. Stuart Allen
(sfa@cs.cornell.edu). |
| |
Reading and explaining a formal theory of lists from the Nuprl 5 library. Contact
Tina Nolte (tan4@cornell.edu). |
| |
Learning to operate JProver, a fully automatic first-order theorem prover. Contact
Dr. Kreitz. |
| 9. |
Reading interesting papers about logic and reporting on them. Here are some examples
that I have copies of: |
| |
- Assigning Meaning to Proofs, R. Constable.
|
| |
- Implementing Metamathematics, R. Constable, Douglas Howe.
|
| |
- A Basis for a Mathematical Theory of Computation, John McCarthy.
|
