CS 410/510 Top: Formal Proof Foundations

Credit Hours:

4/3

Course Coordinator:

Katie Casamento

Course Description:

Explores the role of proof theory in the foundations of logic, mathematics, and computer science. Specific topics covered include natural deduction, constructive logic, and discrete math in a constructive setting. Additional topics may include type theory, basic category theory, and automated theorem proving.

Prerequisites:

Required: CS 251 or equivalent introduction to logic and proofs

Recommended: experience with proofs about computational objects, as discussed in courses like CS 311/581

Goals:

Upon successful completion of this course, students will be able to:

1. Define foundational concepts in proof theory, including propositions, proofs, assumptions, judgements, theorems, and quantifiers.
2. Interpret and construct proofs in a system of natural deduction for first-order and higher-order constructive logic.
3. Explain the relationship between classical and constructive logic in terms of the double-negation translation.
4. Define and prove properties of foundational concepts in constructive mathematics, including sets, relations, equality, functions, ordered pairs, disjoint unions, natural numbers, integers, and lists.

Textbooks:

There are no required textbooks.

References:

Some freely-available readings will be provided on Canvas.