Primitive Recursive Bars Are Inductive August 17, 2016
Logic Seminar, Indiana University. The Church-Turing Thesis is a scientific hypothesis as to the nature of effective computation at lower type; the nature of higher type computability, however, is far from settled and admits many possible models. In the 1920s, L.E.J. Brouwer (the father of Intuitionism) gave a mysterious “proof” of an induction principle for infinite trees called the Bar Theorem, which has many consequences, including a constructive contrapositive to König’s Lemma (the Fan Theorem).
We situate the Bar Theorem more generally as “Brouwer’s Thesis”, a scientific claim about the nature of higher-type computability which may be contrasted with competing explanations, including recursive realizability and Turing machines. Then, we demonstrate using a technique called Effectful Forcing that Brouwer’s Bar Theorem is constructively valid for any bar which can be written in Gödel’s System T of primitive recursive arithmetic of finite type, a very simple programming language.
Slides are available here. This talk is based on my paper, Primitive Recursive Bars Are Inductive; the formal proof of the result described is given in Agda here. My thanks to David Christiansen and Sam Tobin-Hochstadt for hosting!