Forcing in proof theory

Proof theory: the general study of deductive systems Structural proof theory:...with respect to structure, transformations between proofs, normal forms, etc. Hilbert’s program: • Formalize abstract, infinitary, nonconstructive mathematics. • Prove consistency using only finitary methods. More general versions: • Prove consistency relative to constructive theories. • Understand mathematics in constructive terms. • Study mathematical reasoning in “concrete ” terms. – p. 2/88 Proof mining There are • mathematical • computational • foundational • philosophical reasons for modeling mathematical proof in formal terms. Proof mining: using proof theoretic techniques to extract additional mathematical information from inexplicit proofs. – p. 3/88 Proof mining A history of proof mining