Higher-Order Functions and Brouwer's Thesis

DOI10.1017/S0956796821000095arXiv1608.03814WikidataQ126372058 ScholiaQ126372058MaRDI QIDQ6276464

Jonathan Sterling

Publication date: 11 August 2016

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 $(mathbbNomathbbN)omathbbN$ 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 $mathbbNomathbbN$, 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.

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Functionals in proof theory (03F10) Metamathematics of constructive systems (03F50) Combinatory logic and lambda calculus (03B40)

This page was built for publication: Higher-Order Functions and Brouwer's Thesis

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6276464)