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!

Oracles and choice sequences for type theoretic pragmatics October 8, 2014

POP Seminar, Carnegie Mellon University. An adequate type-theoretic semantics for natural language expressions must account for the presuppositions that are expressed by determiners and pronouns. To this end, we extend Type Theory with a choice operator called \(\mathsf{require}\), which functions as a non-deterministic oracle to retrieve the synthesis of a previously-effected verification of a proposition. Then, we give an intuitionistic semantics to this operator by appealing to Brouwer’s theory of the Creating Subject, and eliminate non-determinism via spreads and choice sequences. This is based on joint work with Darryl McAdams, to be published in O. Pombo, A. Nepomuceno, J. Redmond (Ed.) “Epistemology, Knowledge and the Impact of Interaction” (Springer).

Slides are available here. Thanks to Bob Harper for hosting!