Higher-Order Functions and Brouwer's Thesis

TL;DR

This paper presents a new proof of Brouwer's monotone bar theorem for certain functionals in System T, using effectful forcing techniques inspired by programming language concepts, providing an elementary alternative to sheaf-theoretic methods.

Contribution

It introduces an effectful forcing approach to Brouwer's theorem, interpreting System T programs as well-founded dialogue trees with higher-type oracle queries.

Findings

Effectful forcing offers an elementary proof method.

Dialogue tree interpretation connects to Brouwer's bar theorem.

Invariant form of dialogue trees captures barhood construction.

Abstract

Extending Mart\'in Escard\'o's effectful forcing technique, we give a new proof of a well-known result: Brouwer's monotone bar theorem holds for any bar that can be realized by a functional of type $(\mathbb{N} \to \mathbb{N}) \to \mathbb{N}$ in G\"odel's System T. Effectful forcing is an elementary alternative to standard sheaf-theoretic forcing arguments, using ideas from programming languages, including computational effects, monads, the algebra interpretation of call-by-name ${\lambda}$-calculus, and logical relations. Our argument proceeds by interpreting System T programs as well-founded dialogue trees whose nodes branch on a query to an oracle of type $\mathbb{N}\to\mathbb{N}$, lifted to higher type along a call-by-name translation. To connect this interpretation to the bar theorem, we then show that Brouwer's famous "mental constructions" of barhood constitute an invariant form of these dialogue trees in which queries to the oracle are made maximally and in order.