Peter Lumsdaine: Classifying toposes for fun and profit

Abstract

This will be an expository talk, illustrating how topos-theoretic techniques can be applied to turn non-constructive model-theoretic proofs into concrete proof-theoretic arguments.

As the central example, I will take Parikh’s proof (using non-standard models) that if \(\varphi(x, y)\) is a bounded (i.e. \(\Delta_0\)) formula of arithmetic, and “for all \(x\), there exists y such that \(\varphi(x, y)\)” is provable from just induction for \(\Delta_0\) formulas, then there is some fixed \(k\) such that this existence is provably bounded by \(x^k\).