Hostname: page-component-cd9895bd7-dk4vv Total loading time: 0 Render date: 2024-12-23T05:11:58.710Z Has data issue: false hasContentIssue false
  • English
  • Français

WEIHRAUCH GOES BROUWERIAN

Part of: Computability and recursion theory Proof theory and constructive mathematics Distributive lattices Boolean algebras (Boolean rings) General logic

Published online by Cambridge University Press:  30 October 2020

VASCO BRATTKA  and
GUIDO GHERARDI
VASCO BRATTKA
Affiliation:
FACULTY OF COMPUTER SCIENCE UNIVERSITÄT DER BUNDESWEHR MÜNCHENNEUBIBERG, GERMANY DEPARTMENT OF MATHEMATICS & APPLIED MATHEMATICS UNIVERSITY OF CAPE TOWNCAPE TOWN, SOUTH AFRICAE-mail: [email protected]
GUIDO GHERARDI
Affiliation:
DIPARTIMENTO DI FILOSOFIA E COMUNICAZIONE UNIVERSITÀ DI BOLOGNABOLOGNA, ITALYE-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

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

Weihrauch complexitycomputable analysisBrouwer algebraintuitionistic and linear logic

MSC classification

Primary: 03B30: Foundations of classical theories (including reverse mathematics)
Secondary: 03D30: Other degrees and reducibilities 03D78: Computation over the reals 03F52: Linear logic and other substructural logics 03F60: Constructive and recursive analysis 06D20: Heyting algebras
Type
Articles
Information
The Journal of Symbolic Logic , Volume 85 , Issue 4 , December 2020 , pp. 1614 - 1653
Check for updates
Copyright
© The Association for Symbolic Logic 2020

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

Brattka, V., A Galois connection between Turing jumps and limits. Logical Methods in Computer Science, vol. 14 (2018), no. 3:13, pp. 1–37.Google Scholar
Brattka, V., de Brecht, M., and Pauly, A., Closed choice and a uniform low basis theorem. Annals of Pure and Applied Logic, vol. 163 (2012), pp. 986–1008.CrossRefGoogle Scholar
Brattka, V. and Gherardi, G., Weihrauch degrees, omniscience principles and weak computability, this Journal, vol. 76 (2011), no. 1, pp. 143–176.Google Scholar
Brattka, V., Completion of choice. Annals of Pure and Applied Logic, vol. 172 (2021), no. 3, 102914.Google Scholar
Brattka, V., Gherardi, G., and Marcone, A., The Bolzano-Weierstrass theorem is the jump of weak Kőnig’s lemma. Annals of Pure and Applied Logic, vol. 163 (2012), pp. 623–655.CrossRefGoogle Scholar
Brattka, V., Gherardi, G., and Pauly, A., Weihrauch complexity in computable analysis, Handbook of Computability and Complexity in Analysis (Brattka, V. and Hertling, P., editors), Springer, New York, 2021.Google Scholar
Brattka, V., Hendtlass, M., and Kreuzer, A.P., On the uniform computational content of computability theory. Theory of Computing Systems, vol. 61 (2017), no. 4, pp. 1376–1426.CrossRefGoogle Scholar
Brattka, V. and Pauly, A., On the algebraic structure of Weihrauch degrees. Logical Methods in Computer Science, vol. 14 (2018), no. 4:4, pp. 1–36.Google Scholar
Brattka, V. and Rakotoniaina, T., On the uniform computational content of Ramsey’s theorem, this Journal, vol. 82 (2017), 4, pp. 1278–1316,Google Scholar
Dzhafarov, D. D., Joins in the strong Weihrauch degrees. Mathematical Research Letters, vol. 26 (2019), no. 3, pp. 749–767.CrossRefGoogle Scholar
Eršov, J. L., Theory of numberings, Handbook of Computability Theory (Griffor, E. R., editor), Studies in Logic and the Foundations of Mathematics, vol. 140, Elsevier, Amsterdam, 1999, pp. 473–503.CrossRefGoogle Scholar
Galatos, N., Jipsen, P., Kowalski, T., and Ono, H., Residuated Lattices: An Algebraic Glimpse at Substructural Logics, Studies in Logic and the Foundations of Mathematics, vol. 151, Elsevier B. V., Amsterdam, 2007.Google Scholar
Higuchi, K. and Pauly, A., The degree structure of Weihrauch reducibility. Logical Methods in Computer Science, vol. 9 (2013), no. 2:02, pp. 1–17.CrossRefGoogle Scholar
Kechris, A. S., Classical Descriptive Set Theory, Graduate Texts in Mathematics, vol. 156, Springer, Berlin, 1995.CrossRefGoogle Scholar
Kreitz, C. and Weihrauch, K., Theory of representations. Theoretical Computer Science, vol. 38 (1985), pp. 35–53.CrossRefGoogle Scholar
Medvedev, Y. T., Degrees of difficulty of the mass problem. Doklady Akademii Nauk SSSR, vol. 104 (1955), pp. 501–504.Google Scholar
Medvedev, Y. T., Finitive problems. Doklady Akademii Nauk SSSR, vol. 142 (1962), pp. 1015–1018.Google Scholar
Neumann, E. and Pauly, A., A topological view on algebraic computation models. Journal of Complexity, vol. 44 (2018), no. Supplement C, pp. 1–22.CrossRefGoogle Scholar
Pauly, A., On the (semi)lattices induced by continuous reducibilities. Mathematical Logic Quarterly, vol. 56 (2010), no. 5, pp. 488–502.CrossRefGoogle Scholar
Schröder, M., Admissible representations for continuous computations, Ph.D. thesis, Fachbereich Informatik, FernUniversität Hagen, 2002.Google Scholar
Simpson, S. G., Subsystems of Second Order Arithmetic, second ed., Perspectives in Logic, Association for Symbolic Logic, Cambridge University Press, Poughkeepsie, 2009.CrossRefGoogle Scholar
Soare, R. I., Recursively Enumerable Sets and Degrees, Perspectives in Mathematical Logic, Springer, Berlin, 1987.CrossRefGoogle Scholar
Sorbi, A., Embedding Brouwer algebras in the Medvedev lattice. Notre Dame Journal of Formal Logic, vol. 32 (1991), no. 2, pp. 266–275.CrossRefGoogle Scholar
Sorbi, A., The Medvedev lattice of degrees of difficulty, Computability, Enumerability, Unsolvability, London Mathematical Society Lecture Note Series, vol. 224, Cambridge University Press, Cambridge, 1996, pp. 289–312.CrossRefGoogle Scholar
Troelstra, A. S., Lectures on Linear Logic, CSLI Lecture Notes, vol. 29, Stanford University, Center for the Study of Language and Information, Stanford, 1992.Google Scholar
Troelstra, A. S., Comparing the theory of representations and constructive mathematics, Computer Science Logic (Börger, E., Jäger, G., Kleine Büning, H., and Richter, M. M., editors), Lecture Notes in Computer Science, vol. 626, Springer, Berlin, 1992, pp. 382–395.CrossRefGoogle Scholar
Weihrauch, K., Computable Analysis, Springer, Berlin, 2000.CrossRefGoogle Scholar
Yetter, D. N., Quantales and (noncommutative) linear logic, this Journal, vol. 55 (1990), no. 1, pp. 41–64.Google Scholar