The main project for this course will be an approximately 10 page expository paper. Typical examples of appropriate types of papers would be:
- Take a well-studied topic related to proof theory which we didn't have time to cover, read a couple different presentations of it, and then write a paper giving an introduction and overview of the area.
- Read a journal article on a development in an area relating to proof theory and then write a paper explaining one of the main results of that article.
- Read several closely related journal articles and write a paper giving an overview of that line of research.
The expository paper is intended to provide an opportunity to explore connections between proof theory and a subject the student is interested in, so the exact form of the paper is fairly flexible. (For instance, an appropriate programming project would be acceptable.)
- Topic choices due: January 31st
- Paper outline due: February 28th
- First draft due: March 26th
- Last day for (optional) second draft: April 11th
- Final version due: Monday, April 29th, 11 am
Here is a (very non-exhaustive) list of suggested topics:
- Linear logic or other substructural logics (possible sources: Proofs and Types by Girard, Basic Proof Theory by Troelstra and Schwichtenberg, An Introduction to Substructural Logics by Greg Restall)
- The Curry-Howard Isomorphism (possible sources: Proofs and Types by Girard, Basic Proof Theory by Troelstra and Schwichtenberg)
- Model Theory of non-classical logic (possible sources: A Short Introduction to Intuitionistic Logic by Mints)
- Reverse Mathematics (possible sources: Subsystems of Second Order Arithmetic by Stephen Simpson)
- An alternate approach to ordinal analysis, such as ε-substitution (see Gentzen-type systems and Hilbert's epsilon substitution method by Mints) or model-theoretically (see A model-theoretic approach to ordinal analysis by Avigad and Sommer)
- Cut-elimination for an appropriate modal or other logic (possible sources: many papers of this type have been published)
- Foundational concerns (possible sources: In the Light of Logic, by Solomon Feferman)