University of Calgary

UofC Navigation

Official outlines at the end of this page.

Formal proofs in logic and mathematical systems play an important role in several areas of analytic philosophy, including the philosophy of logic and the philosophy of mathematics. The study of formal proofs is the subject of proof theory. It investigates the structure, length, and complexity of formal proofs, operations on formal proofs, relationships between formal proofs in various different proof systems such as the sequent calculus and natural deduction, and special forms formal proofs can have. Formal proofs of theorems in mathematical systems have been used to account for the meaning and truth of these theorems. Proof theoretic results such as consistency proofs have been used for philosophical aims such as to account for the security of mathematical knowledge or to argue for or against various positions in the philosophy of mathematics such asinstrumentalism or the so-called indispensability arguments.

In this course we will study some of the basic methods and results in proof theory. This will include a study of the sequent calculus and the cut-elimination theorem, of natural deduction systems and normal form theorems, and formalizations of mathematics and consistency proofs. The approach will be in part historical: we will study the pioneering work of Gerhard Gentzen in the 1930s and its context in the

development of logic and metamathematics.

Proof theory also has important applications outside of philosophy: in mathematics, computer science, and linguistics. We will touch on some of these applications, depending on student interest.

Phil 279 (Logic I) is a prerequisite for this course.

Readings will be made available via BlackBoard.

Three homework assignments (60%, 20% each) and a final paper (30%) are required to pass the course. There will be no exams. You will give a short presentation on the topic of your final project in the last week of; this presentation will make up 5% of your grade. The remaining 5% will be based on participation in discussion in-class and on the course website.

The final project will consist in either a worked out presentation of an advanced topic (e.g., a proof of a theorem in the metatheory of modal logic, a survey article on some application of modal logic in computer science, logic, or linguistics), or a philosophical paper on a topic related to modal logic. A technical project should run about 7-10 pages (gradstudents: 10-15 pages); a more philosophical paper 10-15 pages (grad students: 15-20 pages). You will give a short presentation on your project/paper (10-20 minutes, depending on class size) in the last week of class. Technical projects may be completed in groups of up to 3 students (undergrads only). If done in a team, the paper should be 10-15 pages long, and the presentation 20-30 minutes shared between team members.

Assignments handed in late will be penalized by the equivalent of one grade point per calendar day.

Collaboration on exercises is encouraged. However, you must write up your own solutions, and obviously you must not simply copy someone else’s solutions. You are also required to list the names of the students with whom you’ve collaborated on the assignment.

Graduate students registered in Phil 679.5 will be expected to complete all the above requirements. Graduate students will be expected to choose more advanced final project topics. Graduate student papers should run 15–20 pages. Collaboration on final projects is allowed, but every graduate student must submit a distinct, self-contained paper, and give a self-contained presentation.

- The Sequent Calculus.
- Cut Elimination.
- Consequences of Cut Elimination.
- Natural Deduction Systems. Relation to Sequent Calculus.
- The Normal Form Theorem.
- Intuitionistic logic.
- Formal Systems of Arithmetic.
- Ordinal Notation Systems.
- Consistency Proofs.
- Philosophical Implications of Consistency Proofs.
- Proof-theoretic Harmony.

File attachments: