Paul Cohen's method of forcing, together with Saul Kripke's related semantics for modal and intuitionistic logic, has had profound effects on a number of branches of mathematical logic, from set theory and model theory to constructive and categorical logic. In this talk, I will argue that forcing also has a place in traditional Hilbert-style proof theory, where the goal is to formalize portions of ordinary mathematics in restricted axiomatic theories, and study those theories in constructive or combinatorial terms. I will discuss the aspects of forcing that are useful in this respect, and offer some examples, including constructivizing model-theoretic arguments, translating classical theories to constructive ones, and obtaining conservation results for subsystems of second-order arithmetic.

An associated paper is available online, http://www.andrew.cmu.edu/~avigad, under "surveys".

For more information about the Penn Logic and Computation Seminar, please see the seminar web page.