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.)

### Timeline

- 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

### Topics

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)