Journal of Symbolic Logic 85 (4):1614-1653 (2020)

We prove that the Weihrauch lattice can be transformed into a Brouwer algebra by the consecutive application of two closure operators in the appropriate order: first completion and then parallelization. The closure operator of completion is a new closure operator that we introduce. It transforms any problem into a total problem on the completion of the respective types, where we allow any value outside of the original domain of the problem. This closure operator is of interest by itself, as it generates a total version of Weihrauch reducibility that is defined like the usual version of Weihrauch reducibility, but in terms of total realizers. From a logical perspective completion can be seen as a way to make problems independent of their premises. Alongside with the completion operator and total Weihrauch reducibility we need to study precomplete representations that are required to describe these concepts. In order to show that the parallelized total Weihrauch lattice forms a Brouwer algebra, we introduce a new multiplicative version of an implication. While the parallelized total Weihrauch lattice forms a Brouwer algebra with this implication, the total Weihrauch lattice fails to be a model of intuitionistic linear logic in two different ways. In order to pinpoint the algebraic reasons for this failure, we introduce the concept of a Weihrauch algebra that allows us to formulate the failure in precise and neat terms. Finally, we show that the Medvedev Brouwer algebra can be embedded into our Brouwer algebra, which also implies that the theory of our Brouwer algebra is Jankov logic.
Keywords No keywords specified (fix it)
Categories (categorize this paper)
DOI 10.1017/jsl.2020.76
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

PhilArchive copy

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 71,355
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

Completion of Choice.Vasco Brattka & Guido Gherardi - 2021 - Annals of Pure and Applied Logic 172 (3):102914.
Closed Choice and a Uniform Low Basis Theorem.Vasco Brattka, Matthew de Brecht & Arno Pauly - 2012 - Annals of Pure and Applied Logic 163 (8):986-1008.
On the (Semi)Lattices Induced by Continuous Reducibilities.Arno Pauly - 2010 - Mathematical Logic Quarterly 56 (5):488-502.
Embedding Brouwer Algebras in the Medvedev Lattice.Andrea Sorbi - 1991 - Notre Dame Journal of Formal Logic 32 (2):266-275.

Add more references

Citations of this work BETA

The Fixed-Point Property for Represented Spaces.Mathieu Hoyrup - 2022 - Annals of Pure and Applied Logic 173 (5):103090.

Add more citations

Similar books and articles

Binomial Pairs, Semi-Brouwerian and Brouwerian Semilattices.Jürgen Schmidt - 1978 - Notre Dame Journal of Formal Logic 19 (3):421-434.
Existentially Closed Brouwerian Semilattices.Luca Carai & Silvio Ghilardi - 2019 - Journal of Symbolic Logic 84 (4):1544-1575.
Some Extensions of the Brouwerian Logic.G. Hughes - 1980 - Bulletin of the Section of Logic 9 (2):78-83.
Completion of Choice.Vasco Brattka & Guido Gherardi - 2021 - Annals of Pure and Applied Logic 172 (3):102914.
Mass Problems and Intuitionism.Stephen G. Simpson - 2008 - Notre Dame Journal of Formal Logic 49 (2):127-136.
A Note on Bar Induction in Constructive Set Theory.Michael Rathjen - 2006 - Mathematical Logic Quarterly 52 (3):253-258.


Added to PP index

Total views
4 ( #1,282,842 of 2,519,622 )

Recent downloads (6 months)
2 ( #271,073 of 2,519,622 )

How can I increase my downloads?


My notes