WEIHRAUCH GOES BROUWERIAN

被引:4
|
作者
Brattka, Vasco [1 ,2 ]
Gherardi, Guido [3 ]
机构
[1] Univ Bundeswehr Munchen, Fac Comp Sci, Neubiberg, Germany
[2] Univ Cape Town, Dept Math & Appl Math, Cape Town, South Africa
[3] Univ Bologna, Dipartimento Filosofia & Comunicaz, Bologna, Italy
基金
新加坡国家研究基金会;
关键词
Weihrauch complexity; computable analysis; Brouwer algebra; intuitionistic and linear logic; UNIFORM COMPUTATIONAL CONTENT;
D O I
10.1017/jsl.2020.76
中图分类号
O1 [数学];
学科分类号
0701 ; 070101 ;
摘要
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.
引用
收藏
页码:1614 / 1653
页数:40
相关论文
共 50 条
  • [1] Brouwerian infinity
    Posy, Carl
    [J]. ONE HUNDRED YEARS OF INTUITIONISM ( 1907- 2007 ): THE CERISY CONFERENCE, 2008, : 21 - 36
  • [2] BROUWERIAN GEOMETRY
    NORDHAUS, EA
    LAPIDUS, L
    [J]. CANADIAN JOURNAL OF MATHEMATICS-JOURNAL CANADIEN DE MATHEMATIQUES, 1954, 6 (02): : 217 - 229
  • [3] Undecidability in Weihrauch Degrees
    Kudinov, Oleg V.
    Selivanov, Victor L.
    Zhukov, Anton V.
    [J]. PROGRAMS, PROOFS, PROCESSES, 2010, 6158 : 256 - +
  • [4] BROUWERIAN INTUITIONISM
    DETLEFSEN, M
    [J]. MIND, 1990, 99 (396) : 501 - 534
  • [5] On linear Brouwerian logics
    Kostrzycka, Zofia
    [J]. MATHEMATICAL LOGIC QUARTERLY, 2014, 60 (4-5) : 304 - 313
  • [6] BROUWERIAN GENERALISED LATTICES
    Kishore, Parimi Radhakrishna
    Mudaso, Demelash Kumsa
    [J]. ADVANCES AND APPLICATIONS IN DISCRETE MATHEMATICS, 2022, 29 (02): : 205 - 222
  • [7] UNDECIDABILITY OF BROUWERIAN SEMILATTICES
    IDZIAK, K
    [J]. ALGEBRA UNIVERSALIS, 1986, 22 (2-3) : 298 - 301
  • [8] EXTENSIONS OF BROUWERIAN SEMILATTICES
    NEMITZ, WC
    [J]. HOUSTON JOURNAL OF MATHEMATICS, 1984, 10 (04): : 545 - 558
  • [9] On Brouwerian bar induction
    Kushner, BA
    [J]. REUNITING THE ANTIPODES - CONSTRUCTIVE AND NONSTANDARD VIEWS OF THE CONTINUUM, 2001, 306 : 119 - 126
  • [10] MINIMAL COVERS IN THE WEIHRAUCH DEGREES
    Lempp, Steffen
    Miller, Joseph s.
    Pauly, Arno
    Soskova, Mariya i.
    Valenti, Manlio
    [J]. PROCEEDINGS OF THE AMERICAN MATHEMATICAL SOCIETY, 2024,